Metamath Proof Explorer

Definition df-plfl

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)

Ref Expression
Assertion 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 >. )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpfl 
 |-  polyFld
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vp 
 |-  p
4 cpl1 
 |-  Poly1
5 1 cv 
 |-  r
6 5 4 cfv 
 |-  ( Poly1 ` r )
7 vs 
 |-  s
8 crsp 
 |-  RSpan
9 7 cv 
 |-  s
10 9 8 cfv 
 |-  ( RSpan ` s )
11 3 cv 
 |-  p
12 11 csn 
 |-  { p }
13 12 10 cfv 
 |-  ( ( RSpan ` s ) ` { p } )
14 vi 
 |-  i
15 vz 
 |-  z
16 cbs 
 |-  Base
17 5 16 cfv 
 |-  ( Base ` r )
18 15 cv 
 |-  z
19 cvsca 
 |-  .s
20 9 19 cfv 
 |-  ( .s ` s )
21 cur 
 |-  1r
22 9 21 cfv 
 |-  ( 1r ` s )
23 18 22 20 co 
 |-  ( z ( .s ` s ) ( 1r ` s ) )
24 cqg 
 |-  ~QG
25 14 cv 
 |-  i
26 9 25 24 co 
 |-  ( s ~QG i )
27 23 26 cec 
 |-  [ ( z ( .s ` s ) ( 1r ` s ) ) ] ( s ~QG i )
28 15 17 27 cmpt 
 |-  ( z e. ( Base ` r ) |-> [ ( z ( .s ` s ) ( 1r ` s ) ) ] ( s ~QG i ) )
29 vf 
 |-  f
30 cqus 
 |-  /s
31 9 26 30 co 
 |-  ( s /s ( s ~QG i ) )
32 vt 
 |-  t
33 32 cv 
 |-  t
34 ctng 
 |-  toNrmGrp
35 vn 
 |-  n
36 cabv 
 |-  AbsVal
37 33 36 cfv 
 |-  ( AbsVal ` t )
38 35 cv 
 |-  n
39 29 cv 
 |-  f
40 38 39 ccom 
 |-  ( n o. f )
41 cnm 
 |-  norm
42 5 41 cfv 
 |-  ( norm ` r )
43 40 42 wceq 
 |-  ( n o. f ) = ( norm ` r )
44 43 35 37 crio 
 |-  ( iota_ n e. ( AbsVal ` t ) ( n o. f ) = ( norm ` r ) )
45 33 44 34 co 
 |-  ( t toNrmGrp ( iota_ n e. ( AbsVal ` t ) ( n o. f ) = ( norm ` r ) ) )
46 csts 
 |-  sSet
47 cple 
 |-  le
48 cnx 
 |-  ndx
49 48 47 cfv 
 |-  ( le ` ndx )
50 33 16 cfv 
 |-  ( Base ` t )
51 vq 
 |-  q
52 cdg1 
 |-  deg1
53 51 cv 
 |-  q
54 5 53 52 co 
 |-  ( r deg1 q )
55 clt 
 |-  <
56 5 11 52 co 
 |-  ( r deg1 p )
57 54 56 55 wbr 
 |-  ( r deg1 q ) < ( r deg1 p )
58 57 51 18 crio 
 |-  ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) )
59 15 50 58 cmpt 
 |-  ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) )
60 vg 
 |-  g
61 60 cv 
 |-  g
62 61 ccnv 
 |-  `' g
63 9 47 cfv 
 |-  ( le ` s )
64 63 61 ccom 
 |-  ( ( le ` s ) o. g )
65 62 64 ccom 
 |-  ( `' g o. ( ( le ` s ) o. g ) )
66 60 59 65 csb 
 |-  [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) )
67 49 66 cop 
 |-  <. ( le ` ndx ) , [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >.
68 45 67 46 co 
 |-  ( ( 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 ) ) >. )
69 32 31 68 csb 
 |-  [_ ( 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 ) ) >. )
70 69 39 cop 
 |-  <. [_ ( 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 >.
71 29 28 70 csb 
 |-  [_ ( 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 >.
72 14 13 71 csb 
 |-  [_ ( ( 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 >.
73 7 6 72 csb 
 |-  [_ ( 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 >.
74 1 3 2 2 73 cmpo 
 |-  ( 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 >. )
75 0 74 wceq 
 |-  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 >. )