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

Definition df-gf 25080
Description: Define the Galois finite field of order  p ^ n. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-gf  |- GF  =  ( p  e.  Prime ,  n  e.  NN  |->  [_ (ℤ/n `  p )  /  r ]_ ( 1st `  (
r splitFld  { [_ (Poly1 `  r
)  /  s ]_ [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x ) } ) ) )
Distinct variable group:    n, p, r, s, x

Detailed syntax breakdown of Definition df-gf
StepHypRef Expression
1 cgf 25071 . 2  class GF
2 vp . . 3  set  p
3 vn . . 3  set  n
4 cprime 13071 . . 3  class  Prime
5 cn 9992 . . 3  class  NN
6 vr . . . 4  set  r
72cv 1651 . . . . 5  class  p
8 czn 16773 . . . . 5  class ℤ/n
97, 8cfv 5446 . . . 4  class  (ℤ/n `  p
)
106cv 1651 . . . . . 6  class  r
11 vs . . . . . . . 8  set  s
12 cpl1 16563 . . . . . . . . 9  class Poly1
1310, 12cfv 5446 . . . . . . . 8  class  (Poly1 `  r
)
14 vx . . . . . . . . 9  set  x
15 cv1 16562 . . . . . . . . . 10  class var1
1610, 15cfv 5446 . . . . . . . . 9  class  (var1 `  r
)
173cv 1651 . . . . . . . . . . . 12  class  n
18 cexp 11374 . . . . . . . . . . . 12  class  ^
197, 17, 18co 6073 . . . . . . . . . . 11  class  ( p ^ n )
2014cv 1651 . . . . . . . . . . 11  class  x
2111cv 1651 . . . . . . . . . . . . 13  class  s
22 cmgp 15640 . . . . . . . . . . . . 13  class mulGrp
2321, 22cfv 5446 . . . . . . . . . . . 12  class  (mulGrp `  s )
24 cmg 14681 . . . . . . . . . . . 12  class .g
2523, 24cfv 5446 . . . . . . . . . . 11  class  (.g `  (mulGrp `  s ) )
2619, 20, 25co 6073 . . . . . . . . . 10  class  ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x )
27 csg 14680 . . . . . . . . . . 11  class  -g
2821, 27cfv 5446 . . . . . . . . . 10  class  ( -g `  s )
2926, 20, 28co 6073 . . . . . . . . 9  class  ( ( ( p ^ n
) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x )
3014, 16, 29csb 3243 . . . . . . . 8  class  [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s )
) x ) (
-g `  s )
x )
3111, 13, 30csb 3243 . . . . . . 7  class  [_ (Poly1 `  r )  /  s ]_ [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x )
3231csn 3806 . . . . . 6  class  { [_ (Poly1 `  r )  /  s ]_ [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x ) }
33 csf 25060 . . . . . 6  class splitFld
3410, 32, 33co 6073 . . . . 5  class  ( r splitFld  { [_ (Poly1 `  r )  / 
s ]_ [_ (var1 `  r
)  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s )
) x ) (
-g `  s )
x ) } )
35 c1st 6339 . . . . 5  class  1st
3634, 35cfv 5446 . . . 4  class  ( 1st `  ( r splitFld  { [_ (Poly1 `  r )  /  s ]_ [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x ) } ) )
376, 9, 36csb 3243 . . 3  class  [_ (ℤ/n `  p
)  /  r ]_ ( 1st `  ( r splitFld  { [_ (Poly1 `  r )  / 
s ]_ [_ (var1 `  r
)  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s )
) x ) (
-g `  s )
x ) } ) )
382, 3, 4, 5, 37cmpt2 6075 . 2  class  ( p  e.  Prime ,  n  e.  NN  |->  [_ (ℤ/n `  p )  /  r ]_ ( 1st `  (
r splitFld  { [_ (Poly1 `  r
)  /  s ]_ [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x ) } ) ) )
391, 38wceq 1652 1  wff GF  =  ( p  e.  Prime ,  n  e.  NN  |->  [_ (ℤ/n `  p )  /  r ]_ ( 1st `  (
r splitFld  { [_ (Poly1 `  r
)  /  s ]_ [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x ) } ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator