Detailed syntax breakdown of Definition df-gf
Step | Hyp | Ref
| Expression |
1 | | cgf 33585 |
. 2
class
GF |
2 | | vp |
. . 3
setvar 𝑝 |
3 | | vn |
. . 3
setvar 𝑛 |
4 | | cprime 16357 |
. . 3
class
ℙ |
5 | | cn 11956 |
. . 3
class
ℕ |
6 | | vr |
. . . 4
setvar 𝑟 |
7 | 2 | cv 1540 |
. . . . 5
class 𝑝 |
8 | | czn 20685 |
. . . . 5
class
ℤ/nℤ |
9 | 7, 8 | cfv 6430 |
. . . 4
class
(ℤ/nℤ‘𝑝) |
10 | 6 | cv 1540 |
. . . . . 6
class 𝑟 |
11 | | vs |
. . . . . . . 8
setvar 𝑠 |
12 | | cpl1 21329 |
. . . . . . . . 9
class
Poly1 |
13 | 10, 12 | cfv 6430 |
. . . . . . . 8
class
(Poly1‘𝑟) |
14 | | vx |
. . . . . . . . 9
setvar 𝑥 |
15 | | cv1 21328 |
. . . . . . . . . 10
class
var1 |
16 | 10, 15 | cfv 6430 |
. . . . . . . . 9
class
(var1‘𝑟) |
17 | 3 | cv 1540 |
. . . . . . . . . . . 12
class 𝑛 |
18 | | cexp 13763 |
. . . . . . . . . . . 12
class
↑ |
19 | 7, 17, 18 | co 7268 |
. . . . . . . . . . 11
class (𝑝↑𝑛) |
20 | 14 | cv 1540 |
. . . . . . . . . . 11
class 𝑥 |
21 | 11 | cv 1540 |
. . . . . . . . . . . . 13
class 𝑠 |
22 | | cmgp 19701 |
. . . . . . . . . . . . 13
class
mulGrp |
23 | 21, 22 | cfv 6430 |
. . . . . . . . . . . 12
class
(mulGrp‘𝑠) |
24 | | cmg 18681 |
. . . . . . . . . . . 12
class
.g |
25 | 23, 24 | cfv 6430 |
. . . . . . . . . . 11
class
(.g‘(mulGrp‘𝑠)) |
26 | 19, 20, 25 | co 7268 |
. . . . . . . . . 10
class ((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥) |
27 | | csg 18560 |
. . . . . . . . . . 11
class
-g |
28 | 21, 27 | cfv 6430 |
. . . . . . . . . 10
class
(-g‘𝑠) |
29 | 26, 20, 28 | co 7268 |
. . . . . . . . 9
class (((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥) |
30 | 14, 16, 29 | csb 3836 |
. . . . . . . 8
class
⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥) |
31 | 11, 13, 30 | csb 3836 |
. . . . . . 7
class
⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥) |
32 | 31 | csn 4566 |
. . . . . 6
class
{⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)} |
33 | | csf 33574 |
. . . . . 6
class
splitFld |
34 | 10, 32, 33 | co 7268 |
. . . . 5
class (𝑟 splitFld
{⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)}) |
35 | | c1st 7815 |
. . . . 5
class
1st |
36 | 34, 35 | cfv 6430 |
. . . 4
class
(1st ‘(𝑟 splitFld
{⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})) |
37 | 6, 9, 36 | csb 3836 |
. . 3
class
⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(1st ‘(𝑟 splitFld
{⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})) |
38 | 2, 3, 4, 5, 37 | cmpo 7270 |
. 2
class (𝑝 ∈ ℙ, 𝑛 ∈ ℕ ↦
⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(1st ‘(𝑟 splitFld
{⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)}))) |
39 | 1, 38 | wceq 1541 |
1
wff GF =
(𝑝 ∈ ℙ, 𝑛 ∈ ℕ ↦
⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(1st ‘(𝑟 splitFld
{⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)}))) |