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

Definition df-gfoo 24000
Description: Define the Galois field of order  p ^  +oo, as a direct limit of the Galois finite fields. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-gfoo  |- GF  =  ( p  e.  Prime  |->  [_ (ℤ/n `  p )  /  r ]_ ( r polySplitLim  ( n  e.  NN  |->  { [_ (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-gfoo
StepHypRef Expression
1 cgfo 23991 . 2  class GF
2 vp . . 3  set  p
3 cprime 12774 . . 3  class  Prime
4 vr . . . 4  set  r
52cv 1631 . . . . 5  class  p
6 czn 16470 . . . . 5  class ℤ/n
75, 6cfv 5271 . . . 4  class  (ℤ/n `  p
)
84cv 1631 . . . . 5  class  r
9 vn . . . . . 6  set  n
10 cn 9762 . . . . . 6  class  NN
11 vs . . . . . . . 8  set  s
12 cpl1 16268 . . . . . . . . 9  class Poly1
138, 12cfv 5271 . . . . . . . 8  class  (Poly1 `  r
)
14 vx . . . . . . . . 9  set  x
15 cv1 16267 . . . . . . . . . 10  class var1
168, 15cfv 5271 . . . . . . . . 9  class  (var1 `  r
)
179cv 1631 . . . . . . . . . . . 12  class  n
18 cexp 11120 . . . . . . . . . . . 12  class  ^
195, 17, 18co 5874 . . . . . . . . . . 11  class  ( p ^ n )
2014cv 1631 . . . . . . . . . . 11  class  x
2111cv 1631 . . . . . . . . . . . . 13  class  s
22 cmgp 15341 . . . . . . . . . . . . 13  class mulGrp
2321, 22cfv 5271 . . . . . . . . . . . 12  class  (mulGrp `  s )
24 cmg 14382 . . . . . . . . . . . 12  class .g
2523, 24cfv 5271 . . . . . . . . . . 11  class  (.g `  (mulGrp `  s ) )
2619, 20, 25co 5874 . . . . . . . . . 10  class  ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x )
27 csg 14381 . . . . . . . . . . 11  class  -g
2821, 27cfv 5271 . . . . . . . . . 10  class  ( -g `  s )
2926, 20, 28co 5874 . . . . . . . . 9  class  ( ( ( p ^ n
) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x )
3014, 16, 29csb 3094 . . . . . . . 8  class  [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s )
) x ) (
-g `  s )
x )
3111, 13, 30csb 3094 . . . . . . 7  class  [_ (Poly1 `  r )  /  s ]_ [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x )
3231csn 3653 . . . . . 6  class  { [_ (Poly1 `  r )  /  s ]_ [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x ) }
339, 10, 32cmpt 4093 . . . . 5  class  ( n  e.  NN  |->  { [_ (Poly1 `  r )  /  s ]_ [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x ) } )
34 cpsl 23980 . . . . 5  class polySplitLim
358, 33, 34co 5874 . . . 4  class  ( r polySplitLim  ( n  e.  NN  |->  { [_ (Poly1 `  r )  / 
s ]_ [_ (var1 `  r
)  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s )
) x ) (
-g `  s )
x ) } ) )
364, 7, 35csb 3094 . . 3  class  [_ (ℤ/n `  p
)  /  r ]_ ( r polySplitLim  ( n  e.  NN  |->  { [_ (Poly1 `  r )  /  s ]_ [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x ) } ) )
372, 3, 36cmpt 4093 . 2  class  ( p  e.  Prime  |->  [_ (ℤ/n `  p
)  /  r ]_ ( r polySplitLim  ( n  e.  NN  |->  { [_ (Poly1 `  r )  /  s ]_ [_ (var1 `  r )  /  x ]_ ( ( ( p ^ n ) (.g `  (mulGrp `  s
) ) x ) ( -g `  s
) x ) } ) ) )
381, 37wceq 1632 1  wff GF  =  ( p  e.  Prime  |->  [_ (ℤ/n `  p )  /  r ]_ ( r polySplitLim  ( n  e.  NN  |->  { [_ (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