Detailed syntax breakdown of Definition df-cytp
Step | Hyp | Ref
| Expression |
1 | | ccytp 40730 |
. 2
class
CytP |
2 | | vn |
. . 3
setvar 𝑛 |
3 | | cn 11830 |
. . 3
class
ℕ |
4 | | ccnfld 20363 |
. . . . . 6
class
ℂfld |
5 | | cpl1 21098 |
. . . . . 6
class
Poly1 |
6 | 4, 5 | cfv 6380 |
. . . . 5
class
(Poly1‘ℂfld) |
7 | | cmgp 19504 |
. . . . 5
class
mulGrp |
8 | 6, 7 | cfv 6380 |
. . . 4
class
(mulGrp‘(Poly1‘ℂfld)) |
9 | | vr |
. . . . 5
setvar 𝑟 |
10 | 4, 7 | cfv 6380 |
. . . . . . . . 9
class
(mulGrp‘ℂfld) |
11 | | cc 10727 |
. . . . . . . . . 10
class
ℂ |
12 | | cc0 10729 |
. . . . . . . . . . 11
class
0 |
13 | 12 | csn 4541 |
. . . . . . . . . 10
class
{0} |
14 | 11, 13 | cdif 3863 |
. . . . . . . . 9
class (ℂ
∖ {0}) |
15 | | cress 16784 |
. . . . . . . . 9
class
↾s |
16 | 10, 14, 15 | co 7213 |
. . . . . . . 8
class
((mulGrp‘ℂfld) ↾s (ℂ
∖ {0})) |
17 | | cod 18916 |
. . . . . . . 8
class
od |
18 | 16, 17 | cfv 6380 |
. . . . . . 7
class
(od‘((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0}))) |
19 | 18 | ccnv 5550 |
. . . . . 6
class ◡(od‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) |
20 | 2 | cv 1542 |
. . . . . . 7
class 𝑛 |
21 | 20 | csn 4541 |
. . . . . 6
class {𝑛} |
22 | 19, 21 | cima 5554 |
. . . . 5
class (◡(od‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) “ {𝑛}) |
23 | | cv1 21097 |
. . . . . . 7
class
var1 |
24 | 4, 23 | cfv 6380 |
. . . . . 6
class
(var1‘ℂfld) |
25 | 9 | cv 1542 |
. . . . . . 7
class 𝑟 |
26 | | cascl 20814 |
. . . . . . . 8
class
algSc |
27 | 6, 26 | cfv 6380 |
. . . . . . 7
class
(algSc‘(Poly1‘ℂfld)) |
28 | 25, 27 | cfv 6380 |
. . . . . 6
class
((algSc‘(Poly1‘ℂfld))‘𝑟) |
29 | | csg 18367 |
. . . . . . 7
class
-g |
30 | 6, 29 | cfv 6380 |
. . . . . 6
class
(-g‘(Poly1‘ℂfld)) |
31 | 24, 28, 30 | co 7213 |
. . . . 5
class
((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)) |
32 | 9, 22, 31 | cmpt 5135 |
. . . 4
class (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) “ {𝑛}) ↦
((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))) |
33 | | cgsu 16945 |
. . . 4
class
Σg |
34 | 8, 32, 33 | co 7213 |
. . 3
class
((mulGrp‘(Poly1‘ℂfld))
Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) “ {𝑛}) ↦
((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))) |
35 | 2, 3, 34 | cmpt 5135 |
. 2
class (𝑛 ∈ ℕ ↦
((mulGrp‘(Poly1‘ℂfld))
Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) “ {𝑛}) ↦
((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))))) |
36 | 1, 35 | wceq 1543 |
1
wff CytP =
(𝑛 ∈ ℕ ↦
((mulGrp‘(Poly1‘ℂfld))
Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) “ {𝑛}) ↦
((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))))) |