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

Definition df-gf 23984
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 23975 . 2  class GF
2 vp . . 3  set  p
3 vn . . 3  set  n
4 cprime 12758 . . 3  class  Prime
5 cn 9746 . . 3  class  NN
6 vr . . . 4  set  r
72cv 1622 . . . . 5  class  p
8 czn 16454 . . . . 5  class ℤ/n
97, 8cfv 5255 . . . 4  class  (ℤ/n `  p
)
106cv 1622 . . . . . 6  class  r
11 vs . . . . . . . 8  set  s
12 cpl1 16252 . . . . . . . . 9  class Poly1
1310, 12cfv 5255 . . . . . . . 8  class  (Poly1 `  r
)
14 vx . . . . . . . . 9  set  x
15 cv1 16251 . . . . . . . . . 10  class var1
1610, 15cfv 5255 . . . . . . . . 9  class  (var1 `  r
)
173cv 1622 . . . . . . . . . . . 12  class  n
18 cexp 11104 . . . . . . . . . . . 12  class  ^
197, 17, 18co 5858 . . . . . . . . . . 11  class  ( p ^ n )
2014cv 1622 . . . . . . . . . . 11  class  x
2111cv 1622 . . . . . . . . . . . . 13  class  s
22 cmgp 15325 . . . . . . . . . . . . 13  class mulGrp
2321, 22cfv 5255 . . . . . . . . . . . 12  class  (mulGrp `  s )
24 cmg 14366 . . . . . . . . . . . 12  class .g
2523, 24cfv 5255 . . . . . . . . . . 11  class  (.g `  (mulGrp `  s ) )
2619, 20, 25co 5858 . . . . . . . . . 10  class  ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x )
27 csg 14365 . . . . . . . . . . 11  class  -g
2821, 27cfv 5255 . . . . . . . . . 10  class  ( -g `  s )
2926, 20, 28co 5858 . . . . . . . . 9  class  ( ( ( p ^ n
) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x )
3014, 16, 29csb 3081 . . . . . . . 8  class  [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s )
) x ) (
-g `  s )
x )
3111, 13, 30csb 3081 . . . . . . 7  class  [_ (Poly1 `  r )  /  s ]_ [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x )
3231csn 3640 . . . . . 6  class  { [_ (Poly1 `  r )  /  s ]_ [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x ) }
33 csf 23964 . . . . . 6  class splitFld
3410, 32, 33co 5858 . . . . 5  class  ( r splitFld  { [_ (Poly1 `  r )  / 
s ]_ [_ (var1 `  r
)  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s )
) x ) (
-g `  s )
x ) } )
35 c1st 6120 . . . . 5  class  1st
3634, 35cfv 5255 . . . 4  class  ( 1st `  ( r splitFld  { [_ (Poly1 `  r )  /  s ]_ [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x ) } ) )
376, 9, 36csb 3081 . . 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 5860 . 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 1623 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