Metamath Proof Explorer

Definition df-gf

Description: Define the Galois finite field of order p ^ n . (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion df-gf 
|- GF = ( p e. Prime , n e. NN |-> [_ ( Z/nZ ` p ) / r ]_ ( 1st ` ( r splitFld { [_ ( Poly1 ` r ) / s ]_ [_ ( var1 ` r ) / x ]_ ( ( ( p ^ n ) ( .g ` ( mulGrp ` s ) ) x ) ( -g ` s ) x ) } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgf 
 |-  GF
1 vp 
 |-  p
2 cprime 
 |-  Prime
3 vn 
 |-  n
4 cn 
 |-  NN
5 czn 
 |-  Z/nZ
6 1 cv 
 |-  p
7 6 5 cfv 
 |-  ( Z/nZ ` p )
8 vr 
 |-  r
9 c1st 
 |-  1st
10 8 cv 
 |-  r
11 csf 
 |-  splitFld
12 cpl1 
 |-  Poly1
13 10 12 cfv 
 |-  ( Poly1 ` r )
14 vs 
 |-  s
15 cv1 
 |-  var1
16 10 15 cfv 
 |-  ( var1 ` r )
17 vx 
 |-  x
18 cexp 
 |-  ^
19 3 cv 
 |-  n
20 6 19 18 co 
 |-  ( p ^ n )
21 cmg 
 |-  .g
22 cmgp 
 |-  mulGrp
23 14 cv 
 |-  s
24 23 22 cfv 
 |-  ( mulGrp ` s )
25 24 21 cfv 
 |-  ( .g ` ( mulGrp ` s ) )
26 17 cv 
 |-  x
27 20 26 25 co 
 |-  ( ( p ^ n ) ( .g ` ( mulGrp ` s ) ) x )
28 csg 
 |-  -g
29 23 28 cfv 
 |-  ( -g ` s )
30 27 26 29 co 
 |-  ( ( ( p ^ n ) ( .g ` ( mulGrp ` s ) ) x ) ( -g ` s ) x )
31 17 16 30 csb 
 |-  [_ ( var1 ` r ) / x ]_ ( ( ( p ^ n ) ( .g ` ( mulGrp ` s ) ) x ) ( -g ` s ) x )
32 14 13 31 csb 
 |-  [_ ( Poly1 ` r ) / s ]_ [_ ( var1 ` r ) / x ]_ ( ( ( p ^ n ) ( .g ` ( mulGrp ` s ) ) x ) ( -g ` s ) x )
33 32 csn 
 |-  { [_ ( Poly1 ` r ) / s ]_ [_ ( var1 ` r ) / x ]_ ( ( ( p ^ n ) ( .g ` ( mulGrp ` s ) ) x ) ( -g ` s ) x ) }
34 10 33 11 co 
 |-  ( r splitFld { [_ ( Poly1 ` r ) / s ]_ [_ ( var1 ` r ) / x ]_ ( ( ( p ^ n ) ( .g ` ( mulGrp ` s ) ) x ) ( -g ` s ) x ) } )
35 34 9 cfv 
 |-  ( 1st ` ( r splitFld { [_ ( Poly1 ` r ) / s ]_ [_ ( var1 ` r ) / x ]_ ( ( ( p ^ n ) ( .g ` ( mulGrp ` s ) ) x ) ( -g ` s ) x ) } ) )
36 8 7 35 csb 
 |-  [_ ( Z/nZ ` p ) / r ]_ ( 1st ` ( r splitFld { [_ ( Poly1 ` r ) / s ]_ [_ ( var1 ` r ) / x ]_ ( ( ( p ^ n ) ( .g ` ( mulGrp ` s ) ) x ) ( -g ` s ) x ) } ) )
37 1 3 2 4 36 cmpo 
 |-  ( p e. Prime , n e. NN |-> [_ ( Z/nZ ` p ) / r ]_ ( 1st ` ( r splitFld { [_ ( Poly1 ` r ) / s ]_ [_ ( var1 ` r ) / x ]_ ( ( ( p ^ n ) ( .g ` ( mulGrp ` s ) ) x ) ( -g ` s ) x ) } ) ) )
38 0 37 wceq 
 |-  GF = ( p e. Prime , n e. NN |-> [_ ( Z/nZ ` p ) / r ]_ ( 1st ` ( r splitFld { [_ ( Poly1 ` r ) / s ]_ [_ ( var1 ` r ) / x ]_ ( ( ( p ^ n ) ( .g ` ( mulGrp ` s ) ) x ) ( -g ` s ) x ) } ) ) )