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	$$⊢{\mathrm{GF}}_{\infty }=\left(p\in \mathbb{P}⟼⦋\mathbb{Z}/p\mathbb{Z}/r⦌\left(r\mathrm{polySplitLim}\left(n\in \mathbb{N}⟼\left\{⦋{\mathrm{Poly}}_1\left(r\right)/s⦌⦋{\mathrm{var}}_1\left(r\right)/x⦌\left(\left(p^n{\cdot }_{{\mathrm{mulGrp}}_s}x\right){-}_{s}x\right)\right\}\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgfo	$$class{\mathrm{GF}}_{\infty }$$
1		vp	$$setvarp$$
2		cprime	$$class\mathbb{P}$$
3		czn	$$class\mathrm{\mathbb{Z}/n\mathbb{Z}}$$
4	1	cv	$$setvarp$$
5	4 3	cfv	$$class\mathbb{Z}/p\mathbb{Z}$$
6		vr	$$setvarr$$
7	6	cv	$$setvarr$$
8		cpsl	$$class\mathrm{polySplitLim}$$
9		vn	$$setvarn$$
10		cn	$$class\mathbb{N}$$
11		cpl1	$$class{\mathrm{Poly}}_1$$
12	7 11	cfv	$$class{\mathrm{Poly}}_1\left(r\right)$$
13		vs	$$setvars$$
14		cv1	$$class{\mathrm{var}}_1$$
15	7 14	cfv	$$class{\mathrm{var}}_1\left(r\right)$$
16		vx	$$setvarx$$
17		cexp	$$class^$$
18	9	cv	$$setvarn$$
19	4 18 17	co	$$class{p}^n$$
20		cmg	$$class{\mathrm{\cdot }}_{𝑔}$$
21		cmgp	$$class\mathrm{mulGrp}$$
22	13	cv	$$setvars$$
23	22 21	cfv	$$class{\mathrm{mulGrp}}_s$$
24	23 20	cfv	$$class{\cdot }_{{\mathrm{mulGrp}}_s}$$
25	16	cv	$$setvarx$$
26	19 25 24	co	$$class\left(p^n{\cdot }_{{\mathrm{mulGrp}}_s}x\right)$$
27		csg	$$class{-}_{𝑔}$$
28	22 27	cfv	$$class{-}_s$$
29	26 25 28	co	$$class\left(\left(p^n{\cdot }_{{\mathrm{mulGrp}}_s}x\right){-}_{s}x\right)$$
30	16 15 29	csb	$$class⦋{\mathrm{var}}_1\left(r\right)/x⦌\left(\left(p^n{\cdot }_{{\mathrm{mulGrp}}_s}x\right){-}_{s}x\right)$$
31	13 12 30	csb	$$class⦋{\mathrm{Poly}}_1\left(r\right)/s⦌⦋{\mathrm{var}}_1\left(r\right)/x⦌\left(\left(p^n{\cdot }_{{\mathrm{mulGrp}}_s}x\right){-}_{s}x\right)$$
32	31	csn	$$class\left\{⦋{\mathrm{Poly}}_1\left(r\right)/s⦌⦋{\mathrm{var}}_1\left(r\right)/x⦌\left(\left(p^n{\cdot }_{{\mathrm{mulGrp}}_s}x\right){-}_{s}x\right)\right\}$$
33	9 10 32	cmpt	$$class\left(n\in \mathbb{N}⟼\left\{⦋{\mathrm{Poly}}_1\left(r\right)/s⦌⦋{\mathrm{var}}_1\left(r\right)/x⦌\left(\left(p^n{\cdot }_{{\mathrm{mulGrp}}_s}x\right){-}_{s}x\right)\right\}\right)$$
34	7 33 8	co	$$class\left(r\mathrm{polySplitLim}\left(n\in \mathbb{N}⟼\left\{⦋{\mathrm{Poly}}_1\left(r\right)/s⦌⦋{\mathrm{var}}_1\left(r\right)/x⦌\left(\left(p^n{\cdot }_{{\mathrm{mulGrp}}_s}x\right){-}_{s}x\right)\right\}\right)\right)$$
35	6 5 34	csb	$$class⦋\mathbb{Z}/p\mathbb{Z}/r⦌\left(r\mathrm{polySplitLim}\left(n\in \mathbb{N}⟼\left\{⦋{\mathrm{Poly}}_1\left(r\right)/s⦌⦋{\mathrm{var}}_1\left(r\right)/x⦌\left(\left(p^n{\cdot }_{{\mathrm{mulGrp}}_s}x\right){-}_{s}x\right)\right\}\right)\right)$$
36	1 2 35	cmpt	$$class\left(p\in \mathbb{P}⟼⦋\mathbb{Z}/p\mathbb{Z}/r⦌\left(r\mathrm{polySplitLim}\left(n\in \mathbb{N}⟼\left\{⦋{\mathrm{Poly}}_1\left(r\right)/s⦌⦋{\mathrm{var}}_1\left(r\right)/x⦌\left(\left(p^n{\cdot }_{{\mathrm{mulGrp}}_s}x\right){-}_{s}x\right)\right\}\right)\right)\right)$$
37	0 36	wceq	$$wff{\mathrm{GF}}_{\infty }=\left(p\in \mathbb{P}⟼⦋\mathbb{Z}/p\mathbb{Z}/r⦌\left(r\mathrm{polySplitLim}\left(n\in \mathbb{N}⟼\left\{⦋{\mathrm{Poly}}_1\left(r\right)/s⦌⦋{\mathrm{var}}_1\left(r\right)/x⦌\left(\left(p^n{\cdot }_{{\mathrm{mulGrp}}_s}x\right){-}_{s}x\right)\right\}\right)\right)\right)$$