Step | Hyp | Ref
| Expression |
1 | | ccytp 41572 |
. 2
class
CytP |
2 | | vn |
. . 3
setvar π |
3 | | cn 12158 |
. . 3
class
β |
4 | | ccnfld 20812 |
. . . . . 6
class
βfld |
5 | | cpl1 21564 |
. . . . . 6
class
Poly1 |
6 | 4, 5 | cfv 6497 |
. . . . 5
class
(Poly1ββfld) |
7 | | cmgp 19901 |
. . . . 5
class
mulGrp |
8 | 6, 7 | cfv 6497 |
. . . 4
class
(mulGrpβ(Poly1ββfld)) |
9 | | vr |
. . . . 5
setvar π |
10 | 4, 7 | cfv 6497 |
. . . . . . . . 9
class
(mulGrpββfld) |
11 | | cc 11054 |
. . . . . . . . . 10
class
β |
12 | | cc0 11056 |
. . . . . . . . . . 11
class
0 |
13 | 12 | csn 4587 |
. . . . . . . . . 10
class
{0} |
14 | 11, 13 | cdif 3908 |
. . . . . . . . 9
class (β
β {0}) |
15 | | cress 17117 |
. . . . . . . . 9
class
βΎs |
16 | 10, 14, 15 | co 7358 |
. . . . . . . 8
class
((mulGrpββfld) βΎs (β
β {0})) |
17 | | cod 19311 |
. . . . . . . 8
class
od |
18 | 16, 17 | cfv 6497 |
. . . . . . 7
class
(odβ((mulGrpββfld) βΎs
(β β {0}))) |
19 | 18 | ccnv 5633 |
. . . . . 6
class β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) |
20 | 2 | cv 1541 |
. . . . . . 7
class π |
21 | 20 | csn 4587 |
. . . . . 6
class {π} |
22 | 19, 21 | cima 5637 |
. . . . 5
class (β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) β {π}) |
23 | | cv1 21563 |
. . . . . . 7
class
var1 |
24 | 4, 23 | cfv 6497 |
. . . . . 6
class
(var1ββfld) |
25 | 9 | cv 1541 |
. . . . . . 7
class π |
26 | | cascl 21274 |
. . . . . . . 8
class
algSc |
27 | 6, 26 | cfv 6497 |
. . . . . . 7
class
(algScβ(Poly1ββfld)) |
28 | 25, 27 | cfv 6497 |
. . . . . 6
class
((algScβ(Poly1ββfld))βπ) |
29 | | csg 18755 |
. . . . . . 7
class
-g |
30 | 6, 29 | cfv 6497 |
. . . . . 6
class
(-gβ(Poly1ββfld)) |
31 | 24, 28, 30 | co 7358 |
. . . . 5
class
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ)) |
32 | 9, 22, 31 | cmpt 5189 |
. . . 4
class (π β (β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) β {π}) β¦
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ))) |
33 | | cgsu 17327 |
. . . 4
class
Ξ£g |
34 | 8, 32, 33 | co 7358 |
. . 3
class
((mulGrpβ(Poly1ββfld))
Ξ£g (π β (β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) β {π}) β¦
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ)))) |
35 | 2, 3, 34 | cmpt 5189 |
. 2
class (π β β β¦
((mulGrpβ(Poly1ββfld))
Ξ£g (π β (β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) β {π}) β¦
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ))))) |
36 | 1, 35 | wceq 1542 |
1
wff CytP =
(π β β β¦
((mulGrpβ(Poly1ββfld))
Ξ£g (π β (β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) β {π}) β¦
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ))))) |