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	⊢ GF = ( 𝑝 ∈ ℙ , 𝑛 ∈ ℕ ↦ ⦋ ( ℤ/nℤ ‘ 𝑝 ) / 𝑟 ⦌ ( 1st ‘ ( 𝑟 splitFld { ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 ) } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgf	⊢ GF
1		vp	⊢ 𝑝
2		cprime	⊢ ℙ
3		vn	⊢ 𝑛
4		cn	⊢ ℕ
5		czn	⊢ ℤ/nℤ
6	1	cv	⊢ 𝑝
7	6 5	cfv	⊢ ( ℤ/nℤ ‘ 𝑝 )
8		vr	⊢ 𝑟
9		c1st	⊢ 1st
10	8	cv	⊢ 𝑟
11		csf	⊢ splitFld
12		cpl1	⊢ Poly1
13	10 12	cfv	⊢ ( Poly1 ‘ 𝑟 )
14		vs	⊢ 𝑠
15		cv1	⊢ var1
16	10 15	cfv	⊢ ( var1 ‘ 𝑟 )
17		vx	⊢ 𝑥
18		cexp	⊢ ↑
19	3	cv	⊢ 𝑛
20	6 19 18	co	⊢ ( 𝑝 ↑ 𝑛 )
21		cmg	⊢ .g
22		cmgp	⊢ mulGrp
23	14	cv	⊢ 𝑠
24	23 22	cfv	⊢ ( mulGrp ‘ 𝑠 )
25	24 21	cfv	⊢ ( .g ‘ ( mulGrp ‘ 𝑠 ) )
26	17	cv	⊢ 𝑥
27	20 26 25	co	⊢ ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 )
28		csg	⊢ -g
29	23 28	cfv	⊢ ( -g ‘ 𝑠 )
30	27 26 29	co	⊢ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 )
31	17 16 30	csb	⊢ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 )
32	14 13 31	csb	⊢ ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 )
33	32	csn	⊢ { ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 ) }
34	10 33 11	co	⊢ ( 𝑟 splitFld { ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 ) } )
35	34 9	cfv	⊢ ( 1st ‘ ( 𝑟 splitFld { ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 ) } ) )
36	8 7 35	csb	⊢ ⦋ ( ℤ/nℤ ‘ 𝑝 ) / 𝑟 ⦌ ( 1st ‘ ( 𝑟 splitFld { ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 ) } ) )
37	1 3 2 4 36	cmpo	⊢ ( 𝑝 ∈ ℙ , 𝑛 ∈ ℕ ↦ ⦋ ( ℤ/nℤ ‘ 𝑝 ) / 𝑟 ⦌ ( 1st ‘ ( 𝑟 splitFld { ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 ) } ) ) )
38	0 37	wceq	⊢ GF = ( 𝑝 ∈ ℙ , 𝑛 ∈ ℕ ↦ ⦋ ( ℤ/nℤ ‘ 𝑝 ) / 𝑟 ⦌ ( 1st ‘ ( 𝑟 splitFld { ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 ) } ) ) )