Definition df-gfoo 35600

Description: Define the Galois field of order 𝑝↑+∞, as a direct limit of the Galois finite fields. (Contributed by Mario Carneiro, 2-Dec-2014.)

Assertion

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

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

Detailed syntax breakdown of Definition df-gfoo

Step	Hyp	Ref	Expression
1		cgfo 35591	. 2 class GF∞
2		vp	. . 3 setvar 𝑝
3		cprime 16691	. . 3 class ℙ
4		vr	. . . 4 setvar 𝑟
5	2	cv 1538	. . . . 5 class 𝑝
6		czn 21476	. . . . 5 class ℤ/nℤ
7	5, 6	cfv 6542	. . . 4 class (ℤ/nℤ‘𝑝)
8	4	cv 1538	. . . . 5 class 𝑟
9		vn	. . . . . 6 setvar 𝑛
10		cn 12249	. . . . . 6 class ℕ
11		vs	. . . . . . . 8 setvar 𝑠
12		cpl1 22141	. . . . . . . . 9 class Poly1
13	8, 12	cfv 6542	. . . . . . . 8 class (Poly1‘𝑟)
14		vx	. . . . . . . . 9 setvar 𝑥
15		cv1 22140	. . . . . . . . . 10 class var1
16	8, 15	cfv 6542	. . . . . . . . 9 class (var1‘𝑟)
17	9	cv 1538	. . . . . . . . . . . 12 class 𝑛
18		cexp 14085	. . . . . . . . . . . 12 class ↑
19	5, 17, 18	co 7414	. . . . . . . . . . 11 class (𝑝↑𝑛)
20	14	cv 1538	. . . . . . . . . . 11 class 𝑥
21	11	cv 1538	. . . . . . . . . . . . 13 class 𝑠
22		cmgp 20106	. . . . . . . . . . . . 13 class mulGrp
23	21, 22	cfv 6542	. . . . . . . . . . . 12 class (mulGrp‘𝑠)
24		cmg 19055	. . . . . . . . . . . 12 class .g
25	23, 24	cfv 6542	. . . . . . . . . . 11 class (.g‘(mulGrp‘𝑠))
26	19, 20, 25	co 7414	. . . . . . . . . 10 class ((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)
27		csg 18923	. . . . . . . . . . 11 class -g
28	21, 27	cfv 6542	. . . . . . . . . 10 class (-g‘𝑠)
29	26, 20, 28	co 7414	. . . . . . . . 9 class (((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)
30	14, 16, 29	csb 3881	. . . . . . . 8 class ⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)
31	11, 13, 30	csb 3881	. . . . . . 7 class ⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)
32	31	csn 4608	. . . . . 6 class {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)}
33	9, 10, 32	cmpt 5207	. . . . 5 class (𝑛 ∈ ℕ ↦ {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})
34		cpsl 35575	. . . . 5 class polySplitLim
35	8, 33, 34	co 7414	. . . 4 class (𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)}))
36	4, 7, 35	csb 3881	. . 3 class ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)}))
37	2, 3, 36	cmpt 5207	. 2 class (𝑝 ∈ ℙ ↦ ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})))
38	1, 37	wceq 1539	1 wff GF∞ = (𝑝 ∈ ℙ ↦ ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})))

This definition is referenced by: (None)