Definition df-gfoo 31550

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

Step	Hyp	Ref	Expression
1		cgfo 31540	. 2 class GF∞
2		vp	. . 3 setvar p
3		cprime 15385	. . 3 class Prime
4		vr	. . . 4 setvar r
5	2	cv 1482	. . . . 5 class p
6		czn 19851	. . . . 5 class ℤ/nℤ
7	5, 6	cfv 5888	. . . 4 class (ℤ/nℤ ` p )
8	4	cv 1482	. . . . 5 class r
9		vn	. . . . . 6 setvar n
10		cn 11020	. . . . . 6 class NN
11		vs	. . . . . . . 8 setvar s
12		cpl1 19547	. . . . . . . . 9 class Poly1
13	8, 12	cfv 5888	. . . . . . . 8 class (Poly1 ` r )
14		vx	. . . . . . . . 9 setvar x
15		cv1 19546	. . . . . . . . . 10 class var1
16	8, 15	cfv 5888	. . . . . . . . 9 class (var1 ` r )
17	9	cv 1482	. . . . . . . . . . . 12 class n
18		cexp 12860	. . . . . . . . . . . 12 class ^
19	5, 17, 18	co 6650	. . . . . . . . . . 11 class ( p ^ n )
20	14	cv 1482	. . . . . . . . . . 11 class x
21	11	cv 1482	. . . . . . . . . . . . 13 class s
22		cmgp 18489	. . . . . . . . . . . . 13 class mulGrp
23	21, 22	cfv 5888	. . . . . . . . . . . 12 class (mulGrp ` s )
24		cmg 17540	. . . . . . . . . . . 12 class .g
25	23, 24	cfv 5888	. . . . . . . . . . 11 class (.g ` (mulGrp ` s ) )
26	19, 20, 25	co 6650	. . . . . . . . . 10 class ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x )
27		csg 17424	. . . . . . . . . . 11 class -g
28	21, 27	cfv 5888	. . . . . . . . . 10 class ( -g ` s )
29	26, 20, 28	co 6650	. . . . . . . . 9 class ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x )
30	14, 16, 29	csb 3533	. . . . . . . 8 class [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x )
31	11, 13, 30	csb 3533	. . . . . . 7 class [_ (Poly1 ` r ) / s ]_ [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x )
32	31	csn 4177	. . . . . 6 class { [_ (Poly1 ` r ) / s ]_ [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x ) }
33	9, 10, 32	cmpt 4729	. . . . 5 class ( n e. NN |-> { [_ (Poly1 ` r ) / s ]_ [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x ) } )
34		cpsl 31529	. . . . 5 class polySplitLim
35	8, 33, 34	co 6650	. . . 4 class ( r polySplitLim ( n e. NN |-> { [_ (Poly1 ` r ) / s ]_ [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x ) } ) )
36	4, 7, 35	csb 3533	. . 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 ) } ) )
37	2, 3, 36	cmpt 4729	. 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 ) } ) ) )
38	1, 37	wceq 1483	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 ) } ) ) )

This definition is referenced by: (None)