Definition df-gfoo 35647

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 35638	. 2 class GF∞
2		vp	. . 3 setvar 𝑝
3		cprime 16647	. . 3 class ℙ
4		vr	. . . 4 setvar 𝑟
5	2	cv 1539	. . . . 5 class 𝑝
6		czn 21418	. . . . 5 class ℤ/nℤ
7	5, 6	cfv 6519	. . . 4 class (ℤ/nℤ‘𝑝)
8	4	cv 1539	. . . . 5 class 𝑟
9		vn	. . . . . 6 setvar 𝑛
10		cn 12197	. . . . . 6 class ℕ
11		vs	. . . . . . . 8 setvar 𝑠
12		cpl1 22067	. . . . . . . . 9 class Poly1
13	8, 12	cfv 6519	. . . . . . . 8 class (Poly1‘𝑟)
14		vx	. . . . . . . . 9 setvar 𝑥
15		cv1 22066	. . . . . . . . . 10 class var1
16	8, 15	cfv 6519	. . . . . . . . 9 class (var1‘𝑟)
17	9	cv 1539	. . . . . . . . . . . 12 class 𝑛
18		cexp 14036	. . . . . . . . . . . 12 class ↑
19	5, 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	9, 10, 32	cmpt 5196	. . . . 5 class (𝑛 ∈ ℕ ↦ {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})
34		cpsl 35622	. . . . 5 class polySplitLim
35	8, 33, 34	co 7394	. . . 4 class (𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)}))
36	4, 7, 35	csb 3870	. . 3 class ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)}))
37	2, 3, 36	cmpt 5196	. 2 class (𝑝 ∈ ℙ ↦ ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})))
38	1, 37	wceq 1540	1 wff GF∞ = (𝑝 ∈ ℙ ↦ ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})))

This definition is referenced by: (None)