Definition df-gf

Description: Define the Galois finite field of order p ^ n . (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Assertion	df-gf	$$⊢\mathrm{GF}=\left(p\in \mathbb{P},n\in \mathbb{N}⟼⦋\mathbb{Z}/p\mathbb{Z}/r⦌1^{st}\left(r\mathrm{splitFld}\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)$$

Detailed syntax breakdown

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