Metamath Proof Explorer

Definition df-gfoo

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)

Ref Expression
Assertion df-gfoo 
|- GF_oo = ( p e. Prime |-> [_ ( Z/nZ ` p ) / r ]_ ( r polySplitLim ( n e. NN |-> { [_ ( Poly1 ` r ) / s ]_ [_ ( var1 ` r ) / x ]_ ( ( ( p ^ n ) ( .g ` ( mulGrp ` s ) ) x ) ( -g ` s ) x ) } ) ) )

Detailed syntax breakdown

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