Detailed syntax breakdown of Definition df-gfoo
Step | Hyp | Ref
| Expression |
1 | | cgfo 33325 |
. 2
class
GF∞ |
2 | | vp |
. . 3
setvar 𝑝 |
3 | | cprime 16233 |
. . 3
class
ℙ |
4 | | vr |
. . . 4
setvar 𝑟 |
5 | 2 | cv 1542 |
. . . . 5
class 𝑝 |
6 | | czn 20474 |
. . . . 5
class
ℤ/nℤ |
7 | 5, 6 | cfv 6385 |
. . . 4
class
(ℤ/nℤ‘𝑝) |
8 | 4 | cv 1542 |
. . . . 5
class 𝑟 |
9 | | vn |
. . . . . 6
setvar 𝑛 |
10 | | cn 11835 |
. . . . . 6
class
ℕ |
11 | | vs |
. . . . . . . 8
setvar 𝑠 |
12 | | cpl1 21103 |
. . . . . . . . 9
class
Poly1 |
13 | 8, 12 | cfv 6385 |
. . . . . . . 8
class
(Poly1‘𝑟) |
14 | | vx |
. . . . . . . . 9
setvar 𝑥 |
15 | | cv1 21102 |
. . . . . . . . . 10
class
var1 |
16 | 8, 15 | cfv 6385 |
. . . . . . . . 9
class
(var1‘𝑟) |
17 | 9 | cv 1542 |
. . . . . . . . . . . 12
class 𝑛 |
18 | | cexp 13640 |
. . . . . . . . . . . 12
class
↑ |
19 | 5, 17, 18 | co 7218 |
. . . . . . . . . . 11
class (𝑝↑𝑛) |
20 | 14 | cv 1542 |
. . . . . . . . . . 11
class 𝑥 |
21 | 11 | cv 1542 |
. . . . . . . . . . . . 13
class 𝑠 |
22 | | cmgp 19509 |
. . . . . . . . . . . . 13
class
mulGrp |
23 | 21, 22 | cfv 6385 |
. . . . . . . . . . . 12
class
(mulGrp‘𝑠) |
24 | | cmg 18493 |
. . . . . . . . . . . 12
class
.g |
25 | 23, 24 | cfv 6385 |
. . . . . . . . . . 11
class
(.g‘(mulGrp‘𝑠)) |
26 | 19, 20, 25 | co 7218 |
. . . . . . . . . 10
class ((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥) |
27 | | csg 18372 |
. . . . . . . . . . 11
class
-g |
28 | 21, 27 | cfv 6385 |
. . . . . . . . . 10
class
(-g‘𝑠) |
29 | 26, 20, 28 | co 7218 |
. . . . . . . . 9
class (((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥) |
30 | 14, 16, 29 | csb 3816 |
. . . . . . . 8
class
⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥) |
31 | 11, 13, 30 | csb 3816 |
. . . . . . 7
class
⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥) |
32 | 31 | csn 4546 |
. . . . . 6
class
{⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)} |
33 | 9, 10, 32 | cmpt 5140 |
. . . . 5
class (𝑛 ∈ ℕ ↦
{⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)}) |
34 | | cpsl 33314 |
. . . . 5
class
polySplitLim |
35 | 8, 33, 34 | co 7218 |
. . . 4
class (𝑟 polySplitLim (𝑛 ∈ ℕ ↦
{⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})) |
36 | 4, 7, 35 | csb 3816 |
. . 3
class
⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦
{⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})) |
37 | 2, 3, 36 | cmpt 5140 |
. 2
class (𝑝 ∈ ℙ ↦
⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦
{⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)}))) |
38 | 1, 37 | wceq 1543 |
1
wff
GF∞ = (𝑝 ∈ ℙ ↦
⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦
{⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)}))) |