Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-plfl Unicode version

Definition df-plfl 23970
Description: Define the field extension that augments a field with the root of the given irreducible polynomial, and extends the norm if one exists and the extension is unique. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-plfl  |- polyFld  =  ( r  e.  _V ,  p  e.  _V  |->  [_ (Poly1 `  r )  /  s ]_ [_ ( (RSpan `  s ) `  {
p } )  / 
i ]_ [_ ( z  e.  ( Base `  r
)  |->  [ ( z ( .s `  s
) ( 1r `  s ) ) ] ( s ~QG  i ) )  / 
f ]_ <. [_ ( s  /.s  (
s ~QG 
i ) )  / 
t ]_ ( ( t toNrmGrp  ( iota_ n  e.  (AbsVal `  t ) ( n  o.  f )  =  ( norm `  r
) ) ) sSet  <. ( le `  ndx ) ,  [_ ( z  e.  ( Base `  t
)  |->  ( iota_ q  e.  z ( r deg1  q )  <  ( r deg1  p ) ) )  /  g ]_ ( `' g  o.  ( ( le `  s )  o.  g
) ) >. ) ,  f >. )
Distinct variable group:    f, g, i, n, p, q, r, s, t, z

Detailed syntax breakdown of Definition df-plfl
StepHypRef Expression
1 cpfl 23962 . 2  class polyFld
2 vr . . 3  set  r
3 vp . . 3  set  p
4 cvv 2788 . . 3  class  _V
5 vs . . . 4  set  s
62cv 1622 . . . . 5  class  r
7 cpl1 16252 . . . . 5  class Poly1
86, 7cfv 5255 . . . 4  class  (Poly1 `  r
)
9 vi . . . . 5  set  i
103cv 1622 . . . . . . 7  class  p
1110csn 3640 . . . . . 6  class  { p }
125cv 1622 . . . . . . 7  class  s
13 crsp 15924 . . . . . . 7  class RSpan
1412, 13cfv 5255 . . . . . 6  class  (RSpan `  s )
1511, 14cfv 5255 . . . . 5  class  ( (RSpan `  s ) `  {
p } )
16 vf . . . . . 6  set  f
17 vz . . . . . . 7  set  z
18 cbs 13148 . . . . . . . 8  class  Base
196, 18cfv 5255 . . . . . . 7  class  ( Base `  r )
2017cv 1622 . . . . . . . . 9  class  z
21 cur 15339 . . . . . . . . . 10  class  1r
2212, 21cfv 5255 . . . . . . . . 9  class  ( 1r
`  s )
23 cvsca 13212 . . . . . . . . . 10  class  .s
2412, 23cfv 5255 . . . . . . . . 9  class  ( .s
`  s )
2520, 22, 24co 5858 . . . . . . . 8  class  ( z ( .s `  s
) ( 1r `  s ) )
269cv 1622 . . . . . . . . 9  class  i
27 cqg 14617 . . . . . . . . 9  class ~QG
2812, 26, 27co 5858 . . . . . . . 8  class  ( s ~QG  i )
2925, 28cec 6658 . . . . . . 7  class  [ ( z ( .s `  s ) ( 1r
`  s ) ) ] ( s ~QG  i )
3017, 19, 29cmpt 4077 . . . . . 6  class  ( z  e.  ( Base `  r
)  |->  [ ( z ( .s `  s
) ( 1r `  s ) ) ] ( s ~QG  i ) )
31 vt . . . . . . . 8  set  t
32 cqus 13408 . . . . . . . . 9  class  /.s
3312, 28, 32co 5858 . . . . . . . 8  class  ( s 
/.s  ( s ~QG  i ) )
3431cv 1622 . . . . . . . . . 10  class  t
35 vn . . . . . . . . . . . . . 14  set  n
3635cv 1622 . . . . . . . . . . . . 13  class  n
3716cv 1622 . . . . . . . . . . . . 13  class  f
3836, 37ccom 4693 . . . . . . . . . . . 12  class  ( n  o.  f )
39 cnm 18099 . . . . . . . . . . . . 13  class  norm
406, 39cfv 5255 . . . . . . . . . . . 12  class  ( norm `  r )
4138, 40wceq 1623 . . . . . . . . . . 11  wff  ( n  o.  f )  =  ( norm `  r
)
42 cabv 15581 . . . . . . . . . . . 12  class AbsVal
4334, 42cfv 5255 . . . . . . . . . . 11  class  (AbsVal `  t )
4441, 35, 43crio 6297 . . . . . . . . . 10  class  ( iota_ n  e.  (AbsVal `  t
) ( n  o.  f )  =  (
norm `  r )
)
45 ctng 18101 . . . . . . . . . 10  class toNrmGrp
4634, 44, 45co 5858 . . . . . . . . 9  class  ( t toNrmGrp  ( iota_ n  e.  (AbsVal `  t ) ( n  o.  f )  =  ( norm `  r
) ) )
47 cnx 13145 . . . . . . . . . . 11  class  ndx
48 cple 13215 . . . . . . . . . . 11  class  le
4947, 48cfv 5255 . . . . . . . . . 10  class  ( le
`  ndx )
50 vg . . . . . . . . . . 11  set  g
5134, 18cfv 5255 . . . . . . . . . . . 12  class  ( Base `  t )
52 vq . . . . . . . . . . . . . . . 16  set  q
5352cv 1622 . . . . . . . . . . . . . . 15  class  q
54 cdg1 19440 . . . . . . . . . . . . . . 15  class deg1
556, 53, 54co 5858 . . . . . . . . . . . . . 14  class  ( r deg1  q )
566, 10, 54co 5858 . . . . . . . . . . . . . 14  class  ( r deg1  p )
57 clt 8867 . . . . . . . . . . . . . 14  class  <
5855, 56, 57wbr 4023 . . . . . . . . . . . . 13  wff  ( r deg1  q )  <  ( r deg1  p )
5958, 52, 20crio 6297 . . . . . . . . . . . 12  class  ( iota_ q  e.  z ( r deg1  q )  <  ( r deg1  p ) )
6017, 51, 59cmpt 4077 . . . . . . . . . . 11  class  ( z  e.  ( Base `  t
)  |->  ( iota_ q  e.  z ( r deg1  q )  <  ( r deg1  p ) ) )
6150cv 1622 . . . . . . . . . . . . 13  class  g
6261ccnv 4688 . . . . . . . . . . . 12  class  `' g
6312, 48cfv 5255 . . . . . . . . . . . . 13  class  ( le
`  s )
6463, 61ccom 4693 . . . . . . . . . . . 12  class  ( ( le `  s )  o.  g )
6562, 64ccom 4693 . . . . . . . . . . 11  class  ( `' g  o.  ( ( le `  s )  o.  g ) )
6650, 60, 65csb 3081 . . . . . . . . . 10  class  [_ (
z  e.  ( Base `  t )  |->  ( iota_ q  e.  z ( r deg1  q )  <  ( r deg1  p ) ) )  / 
g ]_ ( `' g  o.  ( ( le
`  s )  o.  g ) )
6749, 66cop 3643 . . . . . . . . 9  class  <. ( le `  ndx ) , 
[_ ( z  e.  ( Base `  t
)  |->  ( iota_ q  e.  z ( r deg1  q )  <  ( r deg1  p ) ) )  /  g ]_ ( `' g  o.  ( ( le `  s )  o.  g
) ) >.
68 csts 13146 . . . . . . . . 9  class sSet
6946, 67, 68co 5858 . . . . . . . 8  class  ( ( t toNrmGrp  ( iota_ n  e.  (AbsVal `  t )
( n  o.  f
)  =  ( norm `  r ) ) ) sSet  <. ( le `  ndx ) ,  [_ ( z  e.  ( Base `  t
)  |->  ( iota_ q  e.  z ( r deg1  q )  <  ( r deg1  p ) ) )  /  g ]_ ( `' g  o.  ( ( le `  s )  o.  g
) ) >. )
7031, 33, 69csb 3081 . . . . . . 7  class  [_ (
s  /.s  ( s ~QG  i ) )  / 
t ]_ ( ( t toNrmGrp  ( iota_ n  e.  (AbsVal `  t ) ( n  o.  f )  =  ( norm `  r
) ) ) sSet  <. ( le `  ndx ) ,  [_ ( z  e.  ( Base `  t
)  |->  ( iota_ q  e.  z ( r deg1  q )  <  ( r deg1  p ) ) )  /  g ]_ ( `' g  o.  ( ( le `  s )  o.  g
) ) >. )
7170, 37cop 3643 . . . . . 6  class  <. [_ (
s  /.s  ( s ~QG  i ) )  / 
t ]_ ( ( t toNrmGrp  ( iota_ n  e.  (AbsVal `  t ) ( n  o.  f )  =  ( norm `  r
) ) ) sSet  <. ( le `  ndx ) ,  [_ ( z  e.  ( Base `  t
)  |->  ( iota_ q  e.  z ( r deg1  q )  <  ( r deg1  p ) ) )  /  g ]_ ( `' g  o.  ( ( le `  s )  o.  g
) ) >. ) ,  f >.
7216, 30, 71csb 3081 . . . . 5  class  [_ (
z  e.  ( Base `  r )  |->  [ ( z ( .s `  s ) ( 1r
`  s ) ) ] ( s ~QG  i ) )  /  f ]_ <. [_ ( s  /.s  (
s ~QG 
i ) )  / 
t ]_ ( ( t toNrmGrp  ( iota_ n  e.  (AbsVal `  t ) ( n  o.  f )  =  ( norm `  r
) ) ) sSet  <. ( le `  ndx ) ,  [_ ( z  e.  ( Base `  t
)  |->  ( iota_ q  e.  z ( r deg1  q )  <  ( r deg1  p ) ) )  /  g ]_ ( `' g  o.  ( ( le `  s )  o.  g
) ) >. ) ,  f >.
739, 15, 72csb 3081 . . . 4  class  [_ (
(RSpan `  s ) `  { p } )  /  i ]_ [_ (
z  e.  ( Base `  r )  |->  [ ( z ( .s `  s ) ( 1r
`  s ) ) ] ( s ~QG  i ) )  /  f ]_ <. [_ ( s  /.s  (
s ~QG 
i ) )  / 
t ]_ ( ( t toNrmGrp  ( iota_ n  e.  (AbsVal `  t ) ( n  o.  f )  =  ( norm `  r
) ) ) sSet  <. ( le `  ndx ) ,  [_ ( z  e.  ( Base `  t
)  |->  ( iota_ q  e.  z ( r deg1  q )  <  ( r deg1  p ) ) )  /  g ]_ ( `' g  o.  ( ( le `  s )  o.  g
) ) >. ) ,  f >.
745, 8, 73csb 3081 . . 3  class  [_ (Poly1 `  r )  /  s ]_ [_ ( (RSpan `  s ) `  {
p } )  / 
i ]_ [_ ( z  e.  ( Base `  r
)  |->  [ ( z ( .s `  s
) ( 1r `  s ) ) ] ( s ~QG  i ) )  / 
f ]_ <. [_ ( s  /.s  (
s ~QG 
i ) )  / 
t ]_ ( ( t toNrmGrp  ( iota_ n  e.  (AbsVal `  t ) ( n  o.  f )  =  ( norm `  r
) ) ) sSet  <. ( le `  ndx ) ,  [_ ( z  e.  ( Base `  t
)  |->  ( iota_ q  e.  z ( r deg1  q )  <  ( r deg1  p ) ) )  /  g ]_ ( `' g  o.  ( ( le `  s )  o.  g
) ) >. ) ,  f >.
752, 3, 4, 4, 74cmpt2 5860 . 2  class  ( r  e.  _V ,  p  e.  _V  |->  [_ (Poly1 `  r )  / 
s ]_ [_ ( (RSpan `  s ) `  {
p } )  / 
i ]_ [_ ( z  e.  ( Base `  r
)  |->  [ ( z ( .s `  s
) ( 1r `  s ) ) ] ( s ~QG  i ) )  / 
f ]_ <. [_ ( s  /.s  (
s ~QG 
i ) )  / 
t ]_ ( ( t toNrmGrp  ( iota_ n  e.  (AbsVal `  t ) ( n  o.  f )  =  ( norm `  r
) ) ) sSet  <. ( le `  ndx ) ,  [_ ( z  e.  ( Base `  t
)  |->  ( iota_ q  e.  z ( r deg1  q )  <  ( r deg1  p ) ) )  /  g ]_ ( `' g  o.  ( ( le `  s )  o.  g
) ) >. ) ,  f >. )
761, 75wceq 1623 1  wff polyFld  =  ( r  e.  _V ,  p  e.  _V  |->  [_ (Poly1 `  r )  /  s ]_ [_ ( (RSpan `  s ) `  {
p } )  / 
i ]_ [_ ( z  e.  ( Base `  r
)  |->  [ ( z ( .s `  s
) ( 1r `  s ) ) ] ( s ~QG  i ) )  / 
f ]_ <. [_ ( s  /.s  (
s ~QG 
i ) )  / 
t ]_ ( ( t toNrmGrp  ( iota_ n  e.  (AbsVal `  t ) ( n  o.  f )  =  ( norm `  r
) ) ) sSet  <. ( le `  ndx ) ,  [_ ( z  e.  ( Base `  t
)  |->  ( iota_ q  e.  z ( r deg1  q )  <  ( r deg1  p ) ) )  /  g ]_ ( `' g  o.  ( ( le `  s )  o.  g
) ) >. ) ,  f >. )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator