Definition df-gf 35646

Description: Define the Galois finite field of order 𝑝↑𝑛. (Contributed by Mario Carneiro, 2-Dec-2014.)

Assertion

Ref	Expression
df-gf	⊢ GF = (𝑝 ∈ ℙ, 𝑛 ∈ ℕ ↦ ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(1st ‘(𝑟 splitFld {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})))

Distinct variable group:   𝑛,𝑝,𝑟,𝑠,𝑥

Detailed syntax breakdown of Definition df-gf

Step	Hyp	Ref	Expression
1		cgf 35637	. 2 class GF
2		vp	. . 3 setvar 𝑝
3		vn	. . 3 setvar 𝑛
4		cprime 16647	. . 3 class ℙ
5		cn 12197	. . 3 class ℕ
6		vr	. . . 4 setvar 𝑟
7	2	cv 1539	. . . . 5 class 𝑝
8		czn 21418	. . . . 5 class ℤ/nℤ
9	7, 8	cfv 6519	. . . 4 class (ℤ/nℤ‘𝑝)
10	6	cv 1539	. . . . . 6 class 𝑟
11		vs	. . . . . . . 8 setvar 𝑠
12		cpl1 22067	. . . . . . . . 9 class Poly1
13	10, 12	cfv 6519	. . . . . . . 8 class (Poly1‘𝑟)
14		vx	. . . . . . . . 9 setvar 𝑥
15		cv1 22066	. . . . . . . . . 10 class var1
16	10, 15	cfv 6519	. . . . . . . . 9 class (var1‘𝑟)
17	3	cv 1539	. . . . . . . . . . . 12 class 𝑛
18		cexp 14036	. . . . . . . . . . . 12 class ↑
19	7, 17, 18	co 7394	. . . . . . . . . . 11 class (𝑝↑𝑛)
20	14	cv 1539	. . . . . . . . . . 11 class 𝑥
21	11	cv 1539	. . . . . . . . . . . . 13 class 𝑠
22		cmgp 20055	. . . . . . . . . . . . 13 class mulGrp
23	21, 22	cfv 6519	. . . . . . . . . . . 12 class (mulGrp‘𝑠)
24		cmg 19005	. . . . . . . . . . . 12 class .g
25	23, 24	cfv 6519	. . . . . . . . . . 11 class (.g‘(mulGrp‘𝑠))
26	19, 20, 25	co 7394	. . . . . . . . . 10 class ((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)
27		csg 18873	. . . . . . . . . . 11 class -g
28	21, 27	cfv 6519	. . . . . . . . . 10 class (-g‘𝑠)
29	26, 20, 28	co 7394	. . . . . . . . 9 class (((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)
30	14, 16, 29	csb 3870	. . . . . . . 8 class ⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)
31	11, 13, 30	csb 3870	. . . . . . 7 class ⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)
32	31	csn 4597	. . . . . 6 class {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)}
33		csf 35621	. . . . . 6 class splitFld
34	10, 32, 33	co 7394	. . . . 5 class (𝑟 splitFld {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})
35		c1st 7975	. . . . 5 class 1st
36	34, 35	cfv 6519	. . . 4 class (1st ‘(𝑟 splitFld {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)}))
37	6, 9, 36	csb 3870	. . 3 class ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(1st ‘(𝑟 splitFld {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)}))
38	2, 3, 4, 5, 37	cmpo 7396	. 2 class (𝑝 ∈ ℙ, 𝑛 ∈ ℕ ↦ ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(1st ‘(𝑟 splitFld {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})))
39	1, 38	wceq 1540	1 wff GF = (𝑝 ∈ ℙ, 𝑛 ∈ ℕ ↦ ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(1st ‘(𝑟 splitFld {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})))

This definition is referenced by: (None)