Step | Hyp | Ref
| Expression |
1 | | ccytp 42246 |
. 2
class
CytP |
2 | | vn |
. . 3
setvar π |
3 | | cn 12216 |
. . 3
class
β |
4 | | ccnfld 21144 |
. . . . . 6
class
βfld |
5 | | cpl1 21920 |
. . . . . 6
class
Poly1 |
6 | 4, 5 | cfv 6542 |
. . . . 5
class
(Poly1ββfld) |
7 | | cmgp 20028 |
. . . . 5
class
mulGrp |
8 | 6, 7 | cfv 6542 |
. . . 4
class
(mulGrpβ(Poly1ββfld)) |
9 | | vr |
. . . . 5
setvar π |
10 | 4, 7 | cfv 6542 |
. . . . . . . . 9
class
(mulGrpββfld) |
11 | | cc 11110 |
. . . . . . . . . 10
class
β |
12 | | cc0 11112 |
. . . . . . . . . . 11
class
0 |
13 | 12 | csn 4627 |
. . . . . . . . . 10
class
{0} |
14 | 11, 13 | cdif 3944 |
. . . . . . . . 9
class (β
β {0}) |
15 | | cress 17177 |
. . . . . . . . 9
class
βΎs |
16 | 10, 14, 15 | co 7411 |
. . . . . . . 8
class
((mulGrpββfld) βΎs (β
β {0})) |
17 | | cod 19433 |
. . . . . . . 8
class
od |
18 | 16, 17 | cfv 6542 |
. . . . . . 7
class
(odβ((mulGrpββfld) βΎs
(β β {0}))) |
19 | 18 | ccnv 5674 |
. . . . . 6
class β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) |
20 | 2 | cv 1538 |
. . . . . . 7
class π |
21 | 20 | csn 4627 |
. . . . . 6
class {π} |
22 | 19, 21 | cima 5678 |
. . . . 5
class (β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) β {π}) |
23 | | cv1 21919 |
. . . . . . 7
class
var1 |
24 | 4, 23 | cfv 6542 |
. . . . . 6
class
(var1ββfld) |
25 | 9 | cv 1538 |
. . . . . . 7
class π |
26 | | cascl 21626 |
. . . . . . . 8
class
algSc |
27 | 6, 26 | cfv 6542 |
. . . . . . 7
class
(algScβ(Poly1ββfld)) |
28 | 25, 27 | cfv 6542 |
. . . . . 6
class
((algScβ(Poly1ββfld))βπ) |
29 | | csg 18857 |
. . . . . . 7
class
-g |
30 | 6, 29 | cfv 6542 |
. . . . . 6
class
(-gβ(Poly1ββfld)) |
31 | 24, 28, 30 | co 7411 |
. . . . 5
class
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ)) |
32 | 9, 22, 31 | cmpt 5230 |
. . . 4
class (π β (β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) β {π}) β¦
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ))) |
33 | | cgsu 17390 |
. . . 4
class
Ξ£g |
34 | 8, 32, 33 | co 7411 |
. . 3
class
((mulGrpβ(Poly1ββfld))
Ξ£g (π β (β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) β {π}) β¦
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ)))) |
35 | 2, 3, 34 | cmpt 5230 |
. 2
class (π β β β¦
((mulGrpβ(Poly1ββfld))
Ξ£g (π β (β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) β {π}) β¦
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ))))) |
36 | 1, 35 | wceq 1539 |
1
wff CytP =
(π β β β¦
((mulGrpβ(Poly1ββfld))
Ξ£g (π β (β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) β {π}) β¦
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ))))) |