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) (Revised by Thierry Arnoux and Steven Nguyen, 21-Jun-2025)

Ref Expression
Assertion df-plfl 
|- polyFld = ( r e. _V , p e. _V |-> [_ ( Poly1 ` r ) / s ]_ [_ ( ( RSpan ` s ) ` { p } ) / i ]_ [_ ( c e. ( Base ` r ) |-> [ ( c ( .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 ( q ( rem1p ` r ) p ) = q ) ) / 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 vc 
 |-  c
16 cbs 
 |-  Base
17 5 16 cfv 
 |-  ( Base ` r )
18 15 cv 
 |-  c
19 cvsca 
 |-  .s
20 9 19 cfv 
 |-  ( .s ` s )
21 cur 
 |-  1r
22 9 21 cfv 
 |-  ( 1r ` s )
23 18 22 20 co 
 |-  ( c ( .s ` s ) ( 1r ` s ) )
24 cqg 
 |-  ~QG
25 14 cv 
 |-  i
26 9 25 24 co 
 |-  ( s ~QG i )
27 23 26 cec 
 |-  [ ( c ( .s ` s ) ( 1r ` s ) ) ] ( s ~QG i )
28 15 17 27 cmpt 
 |-  ( c e. ( Base ` r ) |-> [ ( c ( .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 vz 
 |-  z
51 33 16 cfv 
 |-  ( Base ` t )
52 vq 
 |-  q
53 50 cv 
 |-  z
54 52 cv 
 |-  q
55 cr1p 
 |-  rem1p
56 5 55 cfv 
 |-  ( rem1p ` r )
57 54 11 56 co 
 |-  ( q ( rem1p ` r ) p )
58 57 54 wceq 
 |-  ( q ( rem1p ` r ) p ) = q
59 58 52 53 crio 
 |-  ( iota_ q e. z ( q ( rem1p ` r ) p ) = q )
60 50 51 59 cmpt 
 |-  ( z e. ( Base ` t ) |-> ( iota_ q e. z ( q ( rem1p ` r ) p ) = q ) )
61 vg 
 |-  g
62 61 cv 
 |-  g
63 62 ccnv 
 |-  `' g
64 9 47 cfv 
 |-  ( le ` s )
65 64 62 ccom 
 |-  ( ( le ` s ) o. g )
66 63 65 ccom 
 |-  ( `' g o. ( ( le ` s ) o. g ) )
67 61 60 66 csb 
 |-  [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( q ( rem1p ` r ) p ) = q ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) )
68 49 67 cop 
 |-  <. ( le ` ndx ) , [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( q ( rem1p ` r ) p ) = q ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >.
69 45 68 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 ( q ( rem1p ` r ) p ) = q ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. )
70 32 31 69 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 ( q ( rem1p ` r ) p ) = q ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. )
71 70 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 ( q ( rem1p ` r ) p ) = q ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >.
72 29 28 71 csb 
 |-  [_ ( c e. ( Base ` r ) |-> [ ( c ( .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 ( q ( rem1p ` r ) p ) = q ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >.
73 14 13 72 csb 
 |-  [_ ( ( RSpan ` s ) ` { p } ) / i ]_ [_ ( c e. ( Base ` r ) |-> [ ( c ( .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 ( q ( rem1p ` r ) p ) = q ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >.
74 7 6 73 csb 
 |-  [_ ( Poly1 ` r ) / s ]_ [_ ( ( RSpan ` s ) ` { p } ) / i ]_ [_ ( c e. ( Base ` r ) |-> [ ( c ( .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 ( q ( rem1p ` r ) p ) = q ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >.
75 1 3 2 2 74 cmpo 
 |-  ( r e. _V , p e. _V |-> [_ ( Poly1 ` r ) / s ]_ [_ ( ( RSpan ` s ) ` { p } ) / i ]_ [_ ( c e. ( Base ` r ) |-> [ ( c ( .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 ( q ( rem1p ` r ) p ) = q ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >. )
76 0 75 wceq 
 |-  polyFld = ( r e. _V , p e. _V |-> [_ ( Poly1 ` r ) / s ]_ [_ ( ( RSpan ` s ) ` { p } ) / i ]_ [_ ( c e. ( Base ` r ) |-> [ ( c ( .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 ( q ( rem1p ` r ) p ) = q ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >. )