Step | Hyp | Ref
| Expression |
1 | | cytpval.p |
. . . . . . 7
β’ π =
(Poly1ββfld) |
2 | 1 | eqcomi 2742 |
. . . . . 6
β’
(Poly1ββfld) = π |
3 | 2 | fveq2i 6846 |
. . . . 5
β’
(mulGrpβ(Poly1ββfld)) =
(mulGrpβπ) |
4 | | cytpval.q |
. . . . 5
β’ π = (mulGrpβπ) |
5 | 3, 4 | eqtr4i 2764 |
. . . 4
β’
(mulGrpβ(Poly1ββfld)) = π |
6 | 5 | a1i 11 |
. . 3
β’ (π = π β
(mulGrpβ(Poly1ββfld)) = π) |
7 | | cytpval.o |
. . . . . . . 8
β’ π = (odβπ) |
8 | | cytpval.t |
. . . . . . . . 9
β’ π =
((mulGrpββfld) βΎs (β β
{0})) |
9 | 8 | fveq2i 6846 |
. . . . . . . 8
β’
(odβπ) =
(odβ((mulGrpββfld) βΎs (β
β {0}))) |
10 | 7, 9 | eqtri 2761 |
. . . . . . 7
β’ π =
(odβ((mulGrpββfld) βΎs (β
β {0}))) |
11 | 10 | cnveqi 5831 |
. . . . . 6
β’ β‘π = β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) |
12 | 11 | imaeq1i 6011 |
. . . . 5
β’ (β‘π β {π}) = (β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) β {π}) |
13 | | sneq 4597 |
. . . . . 6
β’ (π = π β {π} = {π}) |
14 | 13 | imaeq2d 6014 |
. . . . 5
β’ (π = π β (β‘π β {π}) = (β‘π β {π})) |
15 | 12, 14 | eqtr3id 2787 |
. . . 4
β’ (π = π β (β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) β {π}) = (β‘π β {π})) |
16 | | cytpval.x |
. . . . . . 7
β’ π =
(var1ββfld) |
17 | | cytpval.a |
. . . . . . . . 9
β’ π΄ = (algScβπ) |
18 | 1 | fveq2i 6846 |
. . . . . . . . 9
β’
(algScβπ) =
(algScβ(Poly1ββfld)) |
19 | 17, 18 | eqtri 2761 |
. . . . . . . 8
β’ π΄ =
(algScβ(Poly1ββfld)) |
20 | 19 | fveq1i 6844 |
. . . . . . 7
β’ (π΄βπ) =
((algScβ(Poly1ββfld))βπ) |
21 | | cytpval.m |
. . . . . . . 8
β’ β =
(-gβπ) |
22 | 1 | fveq2i 6846 |
. . . . . . . 8
β’
(-gβπ) =
(-gβ(Poly1ββfld)) |
23 | 21, 22 | eqtri 2761 |
. . . . . . 7
β’ β =
(-gβ(Poly1ββfld)) |
24 | 16, 20, 23 | oveq123i 7372 |
. . . . . 6
β’ (π β (π΄βπ)) =
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ)) |
25 | 24 | eqcomi 2742 |
. . . . 5
β’
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ)) = (π β (π΄βπ)) |
26 | 25 | a1i 11 |
. . . 4
β’ (π = π β
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ)) = (π β
(π΄βπ))) |
27 | 15, 26 | mpteq12dv 5197 |
. . 3
β’ (π = π β (π β (β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) β {π}) β¦
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ))) = (π β (β‘π β {π}) β¦ (π β (π΄βπ)))) |
28 | 6, 27 | oveq12d 7376 |
. 2
β’ (π = π β
((mulGrpβ(Poly1ββfld))
Ξ£g (π β (β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) β {π}) β¦
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ)))) = (π Ξ£g (π β (β‘π β {π}) β¦ (π β (π΄βπ))))) |
29 | | df-cytp 41573 |
. 2
β’ CytP =
(π β β β¦
((mulGrpβ(Poly1ββfld))
Ξ£g (π β (β‘(odβ((mulGrpββfld)
βΎs (β β {0}))) β {π}) β¦
((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ))))) |
30 | | ovex 7391 |
. 2
β’ (π Ξ£g
(π β (β‘π β {π}) β¦ (π β (π΄βπ)))) β V |
31 | 28, 29, 30 | fvmpt 6949 |
1
β’ (π β β β
(CytPβπ) = (π Ξ£g
(π β (β‘π β {π}) β¦ (π β (π΄βπ))))) |