Step | Hyp | Ref
| Expression |
1 | | selvvvval.p |
. . . . . 6
β’ π = (πΌ mPoly π
) |
2 | | selvvvval.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
3 | | eqid 2732 |
. . . . . 6
β’ ((πΌ β π½) mPoly π
) = ((πΌ β π½) mPoly π
) |
4 | | eqid 2732 |
. . . . . 6
β’ (π½ mPoly ((πΌ β π½) mPoly π
)) = (π½ mPoly ((πΌ β π½) mPoly π
)) |
5 | | eqid 2732 |
. . . . . 6
β’
(algScβ(π½
mPoly ((πΌ β π½) mPoly π
))) = (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) |
6 | | eqid 2732 |
. . . . . 6
β’
((algScβ(π½
mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) |
7 | | selvvvval.i |
. . . . . 6
β’ (π β πΌ β π) |
8 | | selvvvval.r |
. . . . . 6
β’ (π β π
β CRing) |
9 | | selvvvval.j |
. . . . . 6
β’ (π β π½ β πΌ) |
10 | | selvvvval.f |
. . . . . 6
β’ (π β πΉ β π΅) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | selvval2 41153 |
. . . . 5
β’ (π β (((πΌ selectVars π
)βπ½)βπΉ) = (((πΌ eval (π½ mPoly ((πΌ β π½) mPoly π
)))β(((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β πΉ))β(π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)))))) |
12 | | eqid 2732 |
. . . . . 6
β’ (πΌ eval (π½ mPoly ((πΌ β π½) mPoly π
))) = (πΌ eval (π½ mPoly ((πΌ β π½) mPoly π
))) |
13 | | eqid 2732 |
. . . . . 6
β’ (πΌ mPoly (π½ mPoly ((πΌ β π½) mPoly π
))) = (πΌ mPoly (π½ mPoly ((πΌ β π½) mPoly π
))) |
14 | | eqid 2732 |
. . . . . 6
β’
(Baseβ(πΌ mPoly
(π½ mPoly ((πΌ β π½) mPoly π
)))) = (Baseβ(πΌ mPoly (π½ mPoly ((πΌ β π½) mPoly π
)))) |
15 | | selvvvval.d |
. . . . . 6
β’ π· = {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
16 | | eqid 2732 |
. . . . . 6
β’
(Baseβ(π½ mPoly
((πΌ β π½) mPoly π
))) = (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) |
17 | | eqid 2732 |
. . . . . 6
β’
(mulGrpβ(π½
mPoly ((πΌ β π½) mPoly π
))) = (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) |
18 | | eqid 2732 |
. . . . . 6
β’
(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
)))) =
(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
19 | | eqid 2732 |
. . . . . 6
β’
(.rβ(π½ mPoly ((πΌ β π½) mPoly π
))) = (.rβ(π½ mPoly ((πΌ β π½) mPoly π
))) |
20 | 7, 9 | ssexd 5323 |
. . . . . . 7
β’ (π β π½ β V) |
21 | 7 | difexd 5328 |
. . . . . . . 8
β’ (π β (πΌ β π½) β V) |
22 | 3, 21, 8 | mplcrngd 41115 |
. . . . . . 7
β’ (π β ((πΌ β π½) mPoly π
) β CRing) |
23 | 4, 20, 22 | mplcrngd 41115 |
. . . . . 6
β’ (π β (π½ mPoly ((πΌ β π½) mPoly π
)) β CRing) |
24 | 4 | mplassa 21572 |
. . . . . . . . . . 11
β’ ((π½ β V β§ ((πΌ β π½) mPoly π
) β CRing) β (π½ mPoly ((πΌ β π½) mPoly π
)) β AssAlg) |
25 | 20, 22, 24 | syl2anc 584 |
. . . . . . . . . 10
β’ (π β (π½ mPoly ((πΌ β π½) mPoly π
)) β AssAlg) |
26 | | eqid 2732 |
. . . . . . . . . . 11
β’
(Scalarβ(π½
mPoly ((πΌ β π½) mPoly π
))) = (Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))) |
27 | 5, 26 | asclrhm 21435 |
. . . . . . . . . 10
β’ ((π½ mPoly ((πΌ β π½) mPoly π
)) β AssAlg β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β ((Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))) RingHom (π½ mPoly ((πΌ β π½) mPoly π
)))) |
28 | 25, 27 | syl 17 |
. . . . . . . . 9
β’ (π β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β ((Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))) RingHom (π½ mPoly ((πΌ β π½) mPoly π
)))) |
29 | 3 | mplassa 21572 |
. . . . . . . . . . . 12
β’ (((πΌ β π½) β V β§ π
β CRing) β ((πΌ β π½) mPoly π
) β AssAlg) |
30 | 21, 8, 29 | syl2anc 584 |
. . . . . . . . . . 11
β’ (π β ((πΌ β π½) mPoly π
) β AssAlg) |
31 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(algScβ((πΌ
β π½) mPoly π
)) = (algScβ((πΌ β π½) mPoly π
)) |
32 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(Scalarβ((πΌ
β π½) mPoly π
)) = (Scalarβ((πΌ β π½) mPoly π
)) |
33 | 31, 32 | asclrhm 21435 |
. . . . . . . . . . 11
β’ (((πΌ β π½) mPoly π
) β AssAlg β (algScβ((πΌ β π½) mPoly π
)) β ((Scalarβ((πΌ β π½) mPoly π
)) RingHom ((πΌ β π½) mPoly π
))) |
34 | 30, 33 | syl 17 |
. . . . . . . . . 10
β’ (π β (algScβ((πΌ β π½) mPoly π
)) β ((Scalarβ((πΌ β π½) mPoly π
)) RingHom ((πΌ β π½) mPoly π
))) |
35 | 3, 21, 8 | mplsca 21563 |
. . . . . . . . . . . 12
β’ (π β π
= (Scalarβ((πΌ β π½) mPoly π
))) |
36 | 35 | eqcomd 2738 |
. . . . . . . . . . 11
β’ (π β (Scalarβ((πΌ β π½) mPoly π
)) = π
) |
37 | 4, 20, 22 | mplsca 21563 |
. . . . . . . . . . 11
β’ (π β ((πΌ β π½) mPoly π
) = (Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
38 | 36, 37 | oveq12d 7423 |
. . . . . . . . . 10
β’ (π β ((Scalarβ((πΌ β π½) mPoly π
)) RingHom ((πΌ β π½) mPoly π
)) = (π
RingHom (Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
39 | 34, 38 | eleqtrd 2835 |
. . . . . . . . 9
β’ (π β (algScβ((πΌ β π½) mPoly π
)) β (π
RingHom (Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
40 | | rhmco 20268 |
. . . . . . . . 9
β’
(((algScβ(π½
mPoly ((πΌ β π½) mPoly π
))) β ((Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))) RingHom (π½ mPoly ((πΌ β π½) mPoly π
))) β§ (algScβ((πΌ β π½) mPoly π
)) β (π
RingHom (Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β (π
RingHom (π½ mPoly ((πΌ β π½) mPoly π
)))) |
41 | 28, 39, 40 | syl2anc 584 |
. . . . . . . 8
β’ (π β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β (π
RingHom (π½ mPoly ((πΌ β π½) mPoly π
)))) |
42 | | rhmghm 20254 |
. . . . . . . 8
β’
(((algScβ(π½
mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β (π
RingHom (π½ mPoly ((πΌ β π½) mPoly π
))) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β (π
GrpHom (π½ mPoly ((πΌ β π½) mPoly π
)))) |
43 | | ghmmhm 19096 |
. . . . . . . 8
β’
(((algScβ(π½
mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β (π
GrpHom (π½ mPoly ((πΌ β π½) mPoly π
))) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β (π
MndHom (π½ mPoly ((πΌ β π½) mPoly π
)))) |
44 | 41, 42, 43 | 3syl 18 |
. . . . . . 7
β’ (π β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β (π
MndHom (π½ mPoly ((πΌ β π½) mPoly π
)))) |
45 | 1, 13, 2, 14, 7, 44, 10 | mhmcompl 41117 |
. . . . . 6
β’ (π β (((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β πΉ) β (Baseβ(πΌ mPoly (π½ mPoly ((πΌ β π½) mPoly π
))))) |
46 | | fvexd 6903 |
. . . . . . 7
β’ (π β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β V) |
47 | | eqid 2732 |
. . . . . . . . . . . 12
β’ (π½ mVar ((πΌ β π½) mPoly π
)) = (π½ mVar ((πΌ β π½) mPoly π
)) |
48 | 22 | crngringd 20062 |
. . . . . . . . . . . 12
β’ (π β ((πΌ β π½) mPoly π
) β Ring) |
49 | 4, 47, 16, 20, 48 | mvrf2 21543 |
. . . . . . . . . . 11
β’ (π β (π½ mVar ((πΌ β π½) mPoly π
)):π½βΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
50 | 49 | ffvelcdmda 7083 |
. . . . . . . . . 10
β’ ((π β§ π§ β π½) β ((π½ mVar ((πΌ β π½) mPoly π
))βπ§) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
51 | 50 | adantlr 713 |
. . . . . . . . 9
β’ (((π β§ π§ β πΌ) β§ π§ β π½) β ((π½ mVar ((πΌ β π½) mPoly π
))βπ§) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
52 | | eldif 3957 |
. . . . . . . . . . 11
β’ (π§ β (πΌ β π½) β (π§ β πΌ β§ Β¬ π§ β π½)) |
53 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’
(Baseβ((πΌ
β π½) mPoly π
)) = (Baseβ((πΌ β π½) mPoly π
)) |
54 | 4, 16, 53, 5, 20, 48 | mplasclf 21617 |
. . . . . . . . . . . . 13
β’ (π β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))):(Baseβ((πΌ β π½) mPoly π
))βΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
55 | 54 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (πΌ β π½)) β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))):(Baseβ((πΌ β π½) mPoly π
))βΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
56 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’ ((πΌ β π½) mVar π
) = ((πΌ β π½) mVar π
) |
57 | 8 | crngringd 20062 |
. . . . . . . . . . . . . 14
β’ (π β π
β Ring) |
58 | 3, 56, 53, 21, 57 | mvrf2 21543 |
. . . . . . . . . . . . 13
β’ (π β ((πΌ β π½) mVar π
):(πΌ β π½)βΆ(Baseβ((πΌ β π½) mPoly π
))) |
59 | 58 | ffvelcdmda 7083 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (πΌ β π½)) β (((πΌ β π½) mVar π
)βπ§) β (Baseβ((πΌ β π½) mPoly π
))) |
60 | 55, 59 | ffvelcdmd 7084 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (πΌ β π½)) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
61 | 52, 60 | sylan2br 595 |
. . . . . . . . . 10
β’ ((π β§ (π§ β πΌ β§ Β¬ π§ β π½)) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
62 | 61 | anassrs 468 |
. . . . . . . . 9
β’ (((π β§ π§ β πΌ) β§ Β¬ π§ β π½) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
63 | 51, 62 | ifclda 4562 |
. . . . . . . 8
β’ ((π β§ π§ β πΌ) β if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
64 | 63 | fmpttd 7111 |
. . . . . . 7
β’ (π β (π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)))):πΌβΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
65 | 46, 7, 64 | elmapdd 8831 |
. . . . . 6
β’ (π β (π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)))) β ((Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) βm πΌ)) |
66 | 12, 13, 14, 15, 16, 17, 18, 19, 7, 23, 45, 65 | evlvvval 41142 |
. . . . 5
β’ (π β (((πΌ eval (π½ mPoly ((πΌ β π½) mPoly π
)))β(((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β πΉ))β(π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))) = ((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β πΉ)βπ)(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)))))))) |
67 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(Baseβπ
) =
(Baseβπ
) |
68 | 1, 67, 2, 15, 10 | mplelf 21548 |
. . . . . . . . . . . 12
β’ (π β πΉ:π·βΆ(Baseβπ
)) |
69 | 68 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β πΉ:π·βΆ(Baseβπ
)) |
70 | | simpr 485 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β π β π·) |
71 | 69, 70 | fvco3d 6988 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β ((((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β πΉ)βπ) = (((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
)))β(πΉβπ))) |
72 | 3, 53, 67, 31, 21, 57 | mplasclf 21617 |
. . . . . . . . . . . 12
β’ (π β (algScβ((πΌ β π½) mPoly π
)):(Baseβπ
)βΆ(Baseβ((πΌ β π½) mPoly π
))) |
73 | 72 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (algScβ((πΌ β π½) mPoly π
)):(Baseβπ
)βΆ(Baseβ((πΌ β π½) mPoly π
))) |
74 | 68 | ffvelcdmda 7083 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (πΉβπ) β (Baseβπ
)) |
75 | 73, 74 | fvco3d 6988 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
)))β(πΉβπ)) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)))) |
76 | 71, 75 | eqtrd 2772 |
. . . . . . . . 9
β’ ((π β§ π β π·) β ((((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β πΉ)βπ) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)))) |
77 | 17, 16 | mgpbas 19987 |
. . . . . . . . . . . 12
β’
(Baseβ(π½ mPoly
((πΌ β π½) mPoly π
))) = (Baseβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
78 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
)))) =
(0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
79 | 17, 19 | mgpplusg 19985 |
. . . . . . . . . . . 12
β’
(.rβ(π½ mPoly ((πΌ β π½) mPoly π
))) =
(+gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
80 | 17 | crngmgp 20057 |
. . . . . . . . . . . . . 14
β’ ((π½ mPoly ((πΌ β π½) mPoly π
)) β CRing β (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) β CMnd) |
81 | 23, 80 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) β CMnd) |
82 | 81 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) β CMnd) |
83 | 7 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β πΌ β π) |
84 | 81 | cmnmndd 19666 |
. . . . . . . . . . . . . . 15
β’ (π β (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) β Mnd) |
85 | 84 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β πΌ) β (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) β Mnd) |
86 | 15 | psrbagf 21462 |
. . . . . . . . . . . . . . . 16
β’ (π β π· β π:πΌβΆβ0) |
87 | 86 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β π:πΌβΆβ0) |
88 | 87 | ffvelcdmda 7083 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β πΌ) β (πβπ) β
β0) |
89 | | eqid 2732 |
. . . . . . . . . . . . . . . 16
β’ (π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)))) = (π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)))) |
90 | | eleq1w 2816 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π β (π§ β π½ β π β π½)) |
91 | | fveq2 6888 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π β ((π½ mVar ((πΌ β π½) mPoly π
))βπ§) = ((π½ mVar ((πΌ β π½) mPoly π
))βπ)) |
92 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = π β (((πΌ β π½) mVar π
)βπ§) = (((πΌ β π½) mVar π
)βπ)) |
93 | 92 | fveq2d 6892 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) |
94 | 90, 91, 93 | ifbieq12d 4555 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π β if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))) = if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))) |
95 | | simpr 485 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β πΌ) β π β πΌ) |
96 | 49 | ffvelcdmda 7083 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π½) β ((π½ mVar ((πΌ β π½) mPoly π
))βπ) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
97 | 96 | adantlr 713 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β π½) β ((π½ mVar ((πΌ β π½) mPoly π
))βπ) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
98 | 97 | adantlr 713 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π·) β§ π β πΌ) β§ π β π½) β ((π½ mVar ((πΌ β π½) mPoly π
))βπ) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
99 | | eldif 3957 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πΌ β π½) β (π β πΌ β§ Β¬ π β π½)) |
100 | 54 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (πΌ β π½)) β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))):(Baseβ((πΌ β π½) mPoly π
))βΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
101 | 58 | ffvelcdmda 7083 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (πΌ β π½)) β (((πΌ β π½) mVar π
)βπ) β (Baseβ((πΌ β π½) mPoly π
))) |
102 | 100, 101 | ffvelcdmd 7084 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (πΌ β π½)) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
103 | 99, 102 | sylan2br 595 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β πΌ β§ Β¬ π β π½)) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
104 | 103 | anassrs 468 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β πΌ) β§ Β¬ π β π½) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
105 | 104 | adantllr 717 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π·) β§ π β πΌ) β§ Β¬ π β π½) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
106 | 98, 105 | ifclda 4562 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β πΌ) β if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
107 | 89, 94, 95, 106 | fvmptd3 7018 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β πΌ) β ((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ) = if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))) |
108 | 107, 106 | eqeltrd 2833 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β πΌ) β ((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
109 | 77, 18, 85, 88, 108 | mulgnn0cld 18969 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π β πΌ) β ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
110 | 109 | fmpttd 7111 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))):πΌβΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
111 | 7 | mptexd 7222 |
. . . . . . . . . . . . . 14
β’ (π β (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) β V) |
112 | 111 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) β V) |
113 | | fvexd 6903 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β
(0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β V) |
114 | | funmpt 6583 |
. . . . . . . . . . . . . 14
β’ Fun
(π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) |
115 | 114 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β Fun (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)))) |
116 | 87 | feqmptd 6957 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β π = (π β πΌ β¦ (πβπ))) |
117 | 15 | psrbagfsupp 21464 |
. . . . . . . . . . . . . . 15
β’ (π β π· β π finSupp 0) |
118 | 117 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β π finSupp 0) |
119 | 116, 118 | eqbrtrrd 5171 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (π β πΌ β¦ (πβπ)) finSupp 0) |
120 | | ssidd 4004 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β ((π β πΌ β¦ (πβπ)) supp 0) β ((π β πΌ β¦ (πβπ)) supp 0)) |
121 | 77, 78, 18 | mulg0 18951 |
. . . . . . . . . . . . . . 15
β’ (π‘ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β
(0(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))π‘) = (0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
122 | 121 | adantl 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π‘ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β
(0(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))π‘) = (0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
123 | | 0zd 12566 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β 0 β β€) |
124 | 120, 122,
88, 108, 123 | suppssov1 8179 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) supp
(0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) β ((π β πΌ β¦ (πβπ)) supp 0)) |
125 | 112, 113,
115, 119, 124 | fsuppsssuppgd 41061 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) finSupp
(0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
126 | | disjdifr 4471 |
. . . . . . . . . . . . 13
β’ ((πΌ β π½) β© π½) = β
|
127 | 126 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β ((πΌ β π½) β© π½) = β
) |
128 | | undifr 4481 |
. . . . . . . . . . . . . . 15
β’ (π½ β πΌ β ((πΌ β π½) βͺ π½) = πΌ) |
129 | 9, 128 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (π β ((πΌ β π½) βͺ π½) = πΌ) |
130 | 129 | eqcomd 2738 |
. . . . . . . . . . . . 13
β’ (π β πΌ = ((πΌ β π½) βͺ π½)) |
131 | 130 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β πΌ = ((πΌ β π½) βͺ π½)) |
132 | 77, 78, 79, 82, 83, 110, 125, 127, 131 | gsumsplit 19790 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)))) = (((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ (πΌ β π½)))(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ π½)))) |
133 | | difssd 4131 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (πΌ β π½) β πΌ) |
134 | 133 | resmptd 6038 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ (πΌ β π½)) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)))) |
135 | | eldifi 4125 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πΌ β π½) β π β πΌ) |
136 | 135 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β π β πΌ) |
137 | 135, 106 | sylan2 593 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
138 | 89, 94, 136, 137 | fvmptd3 7018 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ) = if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))) |
139 | | eldifn 4126 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πΌ β π½) β Β¬ π β π½) |
140 | 139 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β Β¬ π β π½) |
141 | 140 | iffalsed 4538 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) |
142 | 138, 141 | eqtrd 2772 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) |
143 | 142 | oveq2d 7421 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)) = ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))) |
144 | 143 | mpteq2dva 5247 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))))) |
145 | 134, 144 | eqtrd 2772 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ (πΌ β π½)) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))))) |
146 | 145 | oveq2d 7421 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ (πΌ β π½))) = ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))))) |
147 | 9 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β π½ β πΌ) |
148 | 147 | resmptd 6038 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ π½) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)))) |
149 | 9 | sselda 3981 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π½) β π β πΌ) |
150 | 149 | adantlr 713 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β π½) β π β πΌ) |
151 | 150, 106 | syldan 591 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β π½) β if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
152 | 89, 94, 150, 151 | fvmptd3 7018 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β π½) β ((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ) = if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))) |
153 | | iftrue 4533 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π½ β if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) = ((π½ mVar ((πΌ β π½) mPoly π
))βπ)) |
154 | 153 | adantl 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β π½) β if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) = ((π½ mVar ((πΌ β π½) mPoly π
))βπ)) |
155 | 152, 154 | eqtrd 2772 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β π½) β ((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ) = ((π½ mVar ((πΌ β π½) mPoly π
))βπ)) |
156 | 155 | oveq2d 7421 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β π½) β ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)) = ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))) |
157 | 156 | mpteq2dva 5247 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))) |
158 | 148, 157 | eqtrd 2772 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ π½) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))) |
159 | 158 | oveq2d 7421 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ π½)) = ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))) |
160 | 146, 159 | oveq12d 7423 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ (πΌ β π½)))(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ π½))) = (((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))))(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))) |
161 | 54 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π·) β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))):(Baseβ((πΌ β π½) mPoly π
))βΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
162 | 4, 20, 30 | mplsca 21563 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((πΌ β π½) mPoly π
) = (Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
163 | 162 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (mulGrpβ((πΌ β π½) mPoly π
)) = (mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
164 | 163 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β
(.gβ(mulGrpβ((πΌ β π½) mPoly π
))) =
(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))) |
165 | 164 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β
(.gβ(mulGrpβ((πΌ β π½) mPoly π
))) =
(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))) |
166 | 165 | oveqd 7422 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)) = ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))) |
167 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . 20
β’
(mulGrpβ((πΌ
β π½) mPoly π
)) = (mulGrpβ((πΌ β π½) mPoly π
)) |
168 | 167, 53 | mgpbas 19987 |
. . . . . . . . . . . . . . . . . . 19
β’
(Baseβ((πΌ
β π½) mPoly π
)) =
(Baseβ(mulGrpβ((πΌ β π½) mPoly π
))) |
169 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . 19
β’
(.gβ(mulGrpβ((πΌ β π½) mPoly π
))) =
(.gβ(mulGrpβ((πΌ β π½) mPoly π
))) |
170 | 167 | crngmgp 20057 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πΌ β π½) mPoly π
) β CRing β (mulGrpβ((πΌ β π½) mPoly π
)) β CMnd) |
171 | 22, 170 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (mulGrpβ((πΌ β π½) mPoly π
)) β CMnd) |
172 | 171 | cmnmndd 19666 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (mulGrpβ((πΌ β π½) mPoly π
)) β Mnd) |
173 | 172 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (mulGrpβ((πΌ β π½) mPoly π
)) β Mnd) |
174 | 135, 88 | sylan2 593 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (πβπ) β
β0) |
175 | 21 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (πΌ β π½) β V) |
176 | 57 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β π
β Ring) |
177 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β π β (πΌ β π½)) |
178 | 3, 56, 53, 175, 176, 177 | mvrcl 21542 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (((πΌ β π½) mVar π
)βπ) β (Baseβ((πΌ β π½) mPoly π
))) |
179 | 168, 169,
173, 174, 178 | mulgnn0cld 18969 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)) β (Baseβ((πΌ β π½) mPoly π
))) |
180 | 166, 179 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)) β (Baseβ((πΌ β π½) mPoly π
))) |
181 | 161, 180 | cofmpt 7126 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))) = (π β (πΌ β π½) β¦ ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))))) |
182 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) = (mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
183 | 182, 17 | rhmmhm 20250 |
. . . . . . . . . . . . . . . . . . . 20
β’
((algScβ(π½
mPoly ((πΌ β π½) mPoly π
))) β ((Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))) RingHom (π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β
((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) MndHom (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
184 | 28, 183 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β
((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) MndHom (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
185 | 184 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β
((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) MndHom (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
186 | 162 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (Baseβ((πΌ β π½) mPoly π
)) = (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
187 | 186 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (Baseβ((πΌ β π½) mPoly π
)) = (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
188 | 178, 187 | eleqtrd 2835 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (((πΌ β π½) mVar π
)βπ) β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
189 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . 20
β’
(Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) = (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
190 | 182, 189 | mgpbas 19987 |
. . . . . . . . . . . . . . . . . . 19
β’
(Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) =
(Baseβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
191 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . 19
β’
(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) =
(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
192 | 190, 191,
18 | mhmmulg 18989 |
. . . . . . . . . . . . . . . . . 18
β’
(((algScβ(π½
mPoly ((πΌ β π½) mPoly π
))) β
((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) MndHom (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β§ (πβπ) β β0 β§ (((πΌ β π½) mVar π
)βπ) β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))) = ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))) |
193 | 185, 174,
188, 192 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))) = ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))) |
194 | 193 | mpteq2dva 5247 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))))) |
195 | 181, 194 | eqtrd 2772 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))))) |
196 | 195 | oveq2d 7421 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g
((algScβ(π½ mPoly
((πΌ β π½) mPoly π
))) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))))) = ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))))) |
197 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’
(0gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) =
(0gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
198 | 162, 22 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . 17
β’ (π β (Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))) β CRing) |
199 | 182 | crngmgp 20057 |
. . . . . . . . . . . . . . . . 17
β’
((Scalarβ(π½
mPoly ((πΌ β π½) mPoly π
))) β CRing β
(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β CMnd) |
200 | 198, 199 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β
(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β CMnd) |
201 | 200 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β CMnd) |
202 | 84 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) β Mnd) |
203 | 21 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (πΌ β π½) β V) |
204 | 184 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β
((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) MndHom (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
205 | 37, 48 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))) β Ring) |
206 | 182 | ringmgp 20055 |
. . . . . . . . . . . . . . . . . . 19
β’
((Scalarβ(π½
mPoly ((πΌ β π½) mPoly π
))) β Ring β
(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β Mnd) |
207 | 205, 206 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β Mnd) |
208 | 207 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β Mnd) |
209 | 190, 191,
208, 174, 188 | mulgnn0cld 18969 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)) β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
210 | 209 | fmpttd 7111 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))):(πΌ β π½)βΆ(Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
211 | 21 | mptexd 7222 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))) β V) |
212 | 211 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))) β V) |
213 | | fvexd 6903 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β
(0gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) β V) |
214 | | funmpt 6583 |
. . . . . . . . . . . . . . . . 17
β’ Fun
(π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))) |
215 | 214 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β Fun (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))) |
216 | 119, 133,
123 | fmptssfisupp 9385 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ (πβπ)) finSupp 0) |
217 | | ssidd 4004 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π·) β ((π β (πΌ β π½) β¦ (πβπ)) supp 0) β ((π β (πΌ β π½) β¦ (πβπ)) supp 0)) |
218 | 186 | eqimssd 4037 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (Baseβ((πΌ β π½) mPoly π
)) β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
219 | 218 | sselda 3981 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π’ β (Baseβ((πΌ β π½) mPoly π
))) β π’ β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
220 | 219 | adantlr 713 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π’ β (Baseβ((πΌ β π½) mPoly π
))) β π’ β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
221 | 190, 197,
191 | mulg0 18951 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ β
(Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β
(0(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))π’) =
(0gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))) |
222 | 220, 221 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π’ β (Baseβ((πΌ β π½) mPoly π
))) β
(0(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))π’) =
(0gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))) |
223 | 101 | adantlr 713 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (((πΌ β π½) mVar π
)βπ) β (Baseβ((πΌ β π½) mPoly π
))) |
224 | 217, 222,
174, 223, 123 | suppssov1 8179 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β ((π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))) supp
(0gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))) β ((π β (πΌ β π½) β¦ (πβπ)) supp 0)) |
225 | 212, 213,
215, 216, 224 | fsuppsssuppgd 41061 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))) finSupp
(0gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))) |
226 | 190, 197,
201, 202, 203, 204, 210, 225 | gsummhm 19800 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g
((algScβ(π½ mPoly
((πΌ β π½) mPoly π
))) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))))) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))))) |
227 | 196, 226 | eqtr3d 2774 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))))) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))))) |
228 | 227 | oveq1d 7420 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))))(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))) = (((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))))(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))) |
229 | 25 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (π½ mPoly ((πΌ β π½) mPoly π
)) β AssAlg) |
230 | 58 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π·) β ((πΌ β π½) mVar π
):(πΌ β π½)βΆ(Baseβ((πΌ β π½) mPoly π
))) |
231 | 230 | ffvelcdmda 7083 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (((πΌ β π½) mVar π
)βπ) β (Baseβ((πΌ β π½) mPoly π
))) |
232 | 217, 222,
174, 231, 123 | suppssov1 8179 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β ((π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))) supp
(0gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))) β ((π β (πΌ β π½) β¦ (πβπ)) supp 0)) |
233 | 212, 213,
215, 216, 232 | fsuppsssuppgd 41061 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))) finSupp
(0gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))) |
234 | 190, 197,
201, 203, 210, 233 | gsumcl 19777 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β ((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))) β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
235 | 20 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β π½ β V) |
236 | 84 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β π½) β (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) β Mnd) |
237 | 150, 88 | syldan 591 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β π½) β (πβπ) β
β0) |
238 | 77, 18, 236, 237, 97 | mulgnn0cld 18969 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β π½) β ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
239 | 238 | fmpttd 7111 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))):π½βΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
240 | 20 | mptexd 7222 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))) β V) |
241 | 240 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))) β V) |
242 | | funmpt 6583 |
. . . . . . . . . . . . . . . 16
β’ Fun
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))) |
243 | 242 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β Fun (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))) |
244 | 119, 147,
123 | fmptssfisupp 9385 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (π β π½ β¦ (πβπ)) finSupp 0) |
245 | | ssidd 4004 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β ((π β π½ β¦ (πβπ)) supp 0) β ((π β π½ β¦ (πβπ)) supp 0)) |
246 | 245, 122,
237, 97, 123 | suppssov1 8179 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β ((π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))) supp
(0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) β ((π β π½ β¦ (πβπ)) supp 0)) |
247 | 241, 113,
243, 244, 246 | fsuppsssuppgd 41061 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))) finSupp
(0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
248 | 77, 78, 82, 235, 239, 247 | gsumcl 19777 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
249 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’ (
Β·π β(π½ mPoly ((πΌ β π½) mPoly π
))) = ( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
))) |
250 | 5, 26, 189, 16, 19, 249 | asclmul1 21431 |
. . . . . . . . . . . . 13
β’ (((π½ mPoly ((πΌ β π½) mPoly π
)) β AssAlg β§
((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))) β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β§ ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β (((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))))(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))) = (((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))))( Β·π β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))) |
251 | 229, 234,
248, 250 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))))(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))) = (((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))))( Β·π β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))) |
252 | 228, 251 | eqtrd 2772 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))))(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))) = (((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))))( Β·π β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))) |
253 | 132, 160,
252 | 3eqtrd 2776 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)))) = (((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))))( Β·π β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))) |
254 | 164 | oveqd 7422 |
. . . . . . . . . . . . . . 15
β’ (π β ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)) = ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))) |
255 | 254 | mpteq2dv 5249 |
. . . . . . . . . . . . . 14
β’ (π β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))) |
256 | 163, 255 | oveq12d 7423 |
. . . . . . . . . . . . 13
β’ (π β ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)))) = ((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))))) |
257 | 256 | eqcomd 2738 |
. . . . . . . . . . . 12
β’ (π β
((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))) = ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))) |
258 | 257 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β ((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))) = ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))) |
259 | 258 | oveq1d 7420 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β
(((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))))( Β·π β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))) = (((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))) |
260 | 253, 259 | eqtrd 2772 |
. . . . . . . . 9
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)))) = (((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))) |
261 | 76, 260 | oveq12d 7423 |
. . . . . . . 8
β’ ((π β§ π β π·) β (((((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β πΉ)βπ)(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))))) = (((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)))(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))) |
262 | 73, 74 | ffvelcdmd 7084 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)) β (Baseβ((πΌ β π½) mPoly π
))) |
263 | 186 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (Baseβ((πΌ β π½) mPoly π
)) = (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
264 | 262, 263 | eleqtrd 2835 |
. . . . . . . . 9
β’ ((π β§ π β π·) β ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)) β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
265 | 4, 20, 48 | mpllmodd 41113 |
. . . . . . . . . . 11
β’ (π β (π½ mPoly ((πΌ β π½) mPoly π
)) β LMod) |
266 | 265 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (π½ mPoly ((πΌ β π½) mPoly π
)) β LMod) |
267 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(0gβ(mulGrpβ((πΌ β π½) mPoly π
))) =
(0gβ(mulGrpβ((πΌ β π½) mPoly π
))) |
268 | 171 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (mulGrpβ((πΌ β π½) mPoly π
)) β CMnd) |
269 | 179 | fmpttd 7111 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))):(πΌ β π½)βΆ(Baseβ((πΌ β π½) mPoly π
))) |
270 | 21 | mptexd 7222 |
. . . . . . . . . . . . . 14
β’ (π β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))) β V) |
271 | 270 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))) β V) |
272 | | fvexd 6903 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β
(0gβ(mulGrpβ((πΌ β π½) mPoly π
))) β V) |
273 | | funmpt 6583 |
. . . . . . . . . . . . . 14
β’ Fun
(π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))) |
274 | 273 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β Fun (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)))) |
275 | 168, 267,
169 | mulg0 18951 |
. . . . . . . . . . . . . . 15
β’ (π β (Baseβ((πΌ β π½) mPoly π
)) β
(0(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))π) =
(0gβ(mulGrpβ((πΌ β π½) mPoly π
)))) |
276 | 275 | adantl 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β (Baseβ((πΌ β π½) mPoly π
))) β
(0(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))π) =
(0gβ(mulGrpβ((πΌ β π½) mPoly π
)))) |
277 | 217, 276,
174, 178, 123 | suppssov1 8179 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β ((π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))) supp
(0gβ(mulGrpβ((πΌ β π½) mPoly π
)))) β ((π β (πΌ β π½) β¦ (πβπ)) supp 0)) |
278 | 271, 272,
274, 216, 277 | fsuppsssuppgd 41061 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))) finSupp
(0gβ(mulGrpβ((πΌ β π½) mPoly π
)))) |
279 | 168, 267,
268, 203, 269, 278 | gsumcl 19777 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)))) β (Baseβ((πΌ β π½) mPoly π
))) |
280 | 279, 263 | eleqtrd 2835 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)))) β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
281 | 16, 26, 249, 189, 266, 280, 248 | lmodvscld 41101 |
. . . . . . . . 9
β’ ((π β§ π β π·) β (((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
282 | 5, 26, 189, 16, 19, 249 | asclmul1 21431 |
. . . . . . . . 9
β’ (((π½ mPoly ((πΌ β π½) mPoly π
)) β AssAlg β§ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)) β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β§ (((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β (((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)))(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))) = (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))) |
283 | 229, 264,
281, 282 | syl3anc 1371 |
. . . . . . . 8
β’ ((π β§ π β π·) β (((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)))(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))) = (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))) |
284 | 261, 283 | eqtrd 2772 |
. . . . . . 7
β’ ((π β§ π β π·) β (((((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β πΉ)βπ)(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))))) = (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))) |
285 | 284 | mpteq2dva 5247 |
. . . . . 6
β’ (π β (π β π· β¦ (((((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β πΉ)βπ)(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)))))) = (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))) |
286 | 285 | oveq2d 7421 |
. . . . 5
β’ (π β ((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β πΉ)βπ)(.rβ(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))))))) = ((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))) |
287 | 11, 66, 286 | 3eqtrd 2776 |
. . . 4
β’ (π β (((πΌ selectVars π
)βπ½)βπΉ) = ((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))) |
288 | 287 | fveq1d 6890 |
. . 3
β’ (π β ((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½)) = (((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))β(π βΎ π½))) |
289 | 288 | fveq1d 6890 |
. 2
β’ (π β (((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½))) = ((((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))β(π βΎ π½))β(π βΎ (πΌ β π½)))) |
290 | | eqid 2732 |
. . . 4
β’
(0gβ((πΌ β π½) mPoly π
)) = (0gβ((πΌ β π½) mPoly π
)) |
291 | 48 | ringcmnd 20094 |
. . . 4
β’ (π β ((πΌ β π½) mPoly π
) β CMnd) |
292 | 8 | crnggrpd 20063 |
. . . . 5
β’ (π β π
β Grp) |
293 | 292 | grpmndd 18828 |
. . . 4
β’ (π β π
β Mnd) |
294 | | ovex 7438 |
. . . . . 6
β’
(β0 βm πΌ) β V |
295 | 15, 294 | rabex2 5333 |
. . . . 5
β’ π· β V |
296 | 295 | a1i 11 |
. . . 4
β’ (π β π· β V) |
297 | | eqid 2732 |
. . . . . 6
β’ {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} = {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β
Fin} |
298 | | eqid 2732 |
. . . . . 6
β’ (π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) = (π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) |
299 | | difssd 4131 |
. . . . . . 7
β’ (π β (πΌ β π½) β πΌ) |
300 | | selvvvval.y |
. . . . . . 7
β’ (π β π β π·) |
301 | 15, 297, 7, 299, 300 | psrbagres 41112 |
. . . . . 6
β’ (π β (π βΎ (πΌ β π½)) β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β
Fin}) |
302 | 3, 53, 297, 298, 21, 292, 301 | mplmapghm 41125 |
. . . . 5
β’ (π β (π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) β (((πΌ β π½) mPoly π
) GrpHom π
)) |
303 | | ghmmhm 19096 |
. . . . 5
β’ ((π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) β (((πΌ β π½) mPoly π
) GrpHom π
) β (π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) β (((πΌ β π½) mPoly π
) MndHom π
)) |
304 | 302, 303 | syl 17 |
. . . 4
β’ (π β (π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) β (((πΌ β π½) mPoly π
) MndHom π
)) |
305 | | eqid 2732 |
. . . . . . . 8
β’ {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β Fin} = {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β
Fin} |
306 | | simpr 485 |
. . . . . . . 8
β’ ((π β§ π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
307 | 4, 53, 16, 305, 306 | mplelf 21548 |
. . . . . . 7
β’ ((π β§ π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β π€:{π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β
Fin}βΆ(Baseβ((πΌ
β π½) mPoly π
))) |
308 | 15, 305, 7, 9, 300 | psrbagres 41112 |
. . . . . . . 8
β’ (π β (π βΎ π½) β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β
Fin}) |
309 | 308 | adantr 481 |
. . . . . . 7
β’ ((π β§ π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β (π βΎ π½) β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β
Fin}) |
310 | 307, 309 | ffvelcdmd 7084 |
. . . . . 6
β’ ((π β§ π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β (π€β(π βΎ π½)) β (Baseβ((πΌ β π½) mPoly π
))) |
311 | 310 | fmpttd 7111 |
. . . . 5
β’ (π β (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))):(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))βΆ(Baseβ((πΌ β π½) mPoly π
))) |
312 | 16, 26, 249, 189, 266, 264, 281 | lmodvscld 41101 |
. . . . . 6
β’ ((π β§ π β π·) β (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
313 | 312 | fmpttd 7111 |
. . . . 5
β’ (π β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))):π·βΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
314 | 311, 313 | fcod 6740 |
. . . 4
β’ (π β ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))):π·βΆ(Baseβ((πΌ β π½) mPoly π
))) |
315 | | fvexd 6903 |
. . . . 5
β’ (π β
(0gβ((πΌ
β π½) mPoly π
)) β V) |
316 | 23 | crngringd 20062 |
. . . . . 6
β’ (π β (π½ mPoly ((πΌ β π½) mPoly π
)) β Ring) |
317 | | eqid 2732 |
. . . . . . 7
β’
(0gβ(π½ mPoly ((πΌ β π½) mPoly π
))) = (0gβ(π½ mPoly ((πΌ β π½) mPoly π
))) |
318 | 16, 317 | ring0cl 20077 |
. . . . . 6
β’ ((π½ mPoly ((πΌ β π½) mPoly π
)) β Ring β
(0gβ(π½
mPoly ((πΌ β π½) mPoly π
))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
319 | 316, 318 | syl 17 |
. . . . 5
β’ (π β
(0gβ(π½
mPoly ((πΌ β π½) mPoly π
))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
320 | | ssidd 4004 |
. . . . 5
β’ (π β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
321 | 295 | mptex 7221 |
. . . . . . 7
β’ (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))) β V |
322 | 321 | a1i 11 |
. . . . . 6
β’ (π β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))) β V) |
323 | | fvexd 6903 |
. . . . . 6
β’ (π β
(0gβ(π½
mPoly ((πΌ β π½) mPoly π
))) β V) |
324 | | funmpt 6583 |
. . . . . . 7
β’ Fun
(π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))) |
325 | 324 | a1i 11 |
. . . . . 6
β’ (π β Fun (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))) |
326 | 295 | mptex 7221 |
. . . . . . . 8
β’ (π β π· β¦ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))) β V |
327 | 326 | a1i 11 |
. . . . . . 7
β’ (π β (π β π· β¦ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))) β V) |
328 | | fvexd 6903 |
. . . . . . 7
β’ (π β
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β V) |
329 | | funmpt 6583 |
. . . . . . . 8
β’ Fun
(π β π· β¦ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))) |
330 | 329 | a1i 11 |
. . . . . . 7
β’ (π β Fun (π β π· β¦ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)))) |
331 | | eqid 2732 |
. . . . . . . 8
β’
(0gβπ
) = (0gβπ
) |
332 | 1, 2, 331, 10, 8 | mplelsfi 21545 |
. . . . . . 7
β’ (π β πΉ finSupp (0gβπ
)) |
333 | | ssidd 4004 |
. . . . . . . . . . 11
β’ (π β (πΉ supp (0gβπ
)) β (πΉ supp (0gβπ
))) |
334 | | fvexd 6903 |
. . . . . . . . . . 11
β’ (π β (0gβπ
) β V) |
335 | 68, 333, 10, 334 | suppssrg 8178 |
. . . . . . . . . 10
β’ ((π β§ π β (π· β (πΉ supp (0gβπ
)))) β (πΉβπ) = (0gβπ
)) |
336 | 335 | fveq2d 6892 |
. . . . . . . . 9
β’ ((π β§ π β (π· β (πΉ supp (0gβπ
)))) β ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)) = ((algScβ((πΌ β π½) mPoly π
))β(0gβπ
))) |
337 | 3, 31, 331, 290, 21, 57 | mplascl0 41123 |
. . . . . . . . . . 11
β’ (π β ((algScβ((πΌ β π½) mPoly π
))β(0gβπ
)) =
(0gβ((πΌ
β π½) mPoly π
))) |
338 | 162 | fveq2d 6892 |
. . . . . . . . . . 11
β’ (π β
(0gβ((πΌ
β π½) mPoly π
)) =
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
339 | 337, 338 | eqtrd 2772 |
. . . . . . . . . 10
β’ (π β ((algScβ((πΌ β π½) mPoly π
))β(0gβπ
)) =
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
340 | 339 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β (π· β (πΉ supp (0gβπ
)))) β ((algScβ((πΌ β π½) mPoly π
))β(0gβπ
)) =
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
341 | 336, 340 | eqtrd 2772 |
. . . . . . . 8
β’ ((π β§ π β (π· β (πΉ supp (0gβπ
)))) β ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)) =
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
342 | 341, 296 | suppss2 8181 |
. . . . . . 7
β’ (π β ((π β π· β¦ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))) supp
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) β (πΉ supp (0gβπ
))) |
343 | 327, 328,
330, 332, 342 | fsuppsssuppgd 41061 |
. . . . . 6
β’ (π β (π β π· β¦ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))) finSupp
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
344 | | ssidd 4004 |
. . . . . . 7
β’ (π β ((π β π· β¦ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))) supp
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) β ((π β π· β¦ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))) supp
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))) |
345 | | eqid 2732 |
. . . . . . . . 9
β’
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) =
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
346 | 16, 26, 249, 345, 317 | lmod0vs 20497 |
. . . . . . . 8
β’ (((π½ mPoly ((πΌ β π½) mPoly π
)) β LMod β§ π β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β
((0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))π) = (0gβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
347 | 265, 346 | sylan 580 |
. . . . . . 7
β’ ((π β§ π β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β
((0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))π) = (0gβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
348 | 344, 347,
262, 281, 328 | suppssov1 8179 |
. . . . . 6
β’ (π β ((π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))) supp (0gβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β ((π β π· β¦ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))) supp
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))) |
349 | 322, 323,
325, 343, 348 | fsuppsssuppgd 41061 |
. . . . 5
β’ (π β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))) finSupp (0gβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
350 | | eqid 2732 |
. . . . . . . 8
β’ (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) = (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) |
351 | 22 | crnggrpd 20063 |
. . . . . . . 8
β’ (π β ((πΌ β π½) mPoly π
) β Grp) |
352 | 4, 16, 305, 350, 20, 351, 308 | mplmapghm 41125 |
. . . . . . 7
β’ (π β (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β ((π½ mPoly ((πΌ β π½) mPoly π
)) GrpHom ((πΌ β π½) mPoly π
))) |
353 | | ghmmhm 19096 |
. . . . . . 7
β’ ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β ((π½ mPoly ((πΌ β π½) mPoly π
)) GrpHom ((πΌ β π½) mPoly π
)) β (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β ((π½ mPoly ((πΌ β π½) mPoly π
)) MndHom ((πΌ β π½) mPoly π
))) |
354 | 352, 353 | syl 17 |
. . . . . 6
β’ (π β (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β ((π½ mPoly ((πΌ β π½) mPoly π
)) MndHom ((πΌ β π½) mPoly π
))) |
355 | 317, 290 | mhm0 18676 |
. . . . . 6
β’ ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β ((π½ mPoly ((πΌ β π½) mPoly π
)) MndHom ((πΌ β π½) mPoly π
)) β ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½)))β(0gβ(π½ mPoly ((πΌ β π½) mPoly π
)))) = (0gβ((πΌ β π½) mPoly π
))) |
356 | 354, 355 | syl 17 |
. . . . 5
β’ (π β ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½)))β(0gβ(π½ mPoly ((πΌ β π½) mPoly π
)))) = (0gβ((πΌ β π½) mPoly π
))) |
357 | 315, 319,
313, 311, 320, 296, 46, 349, 356 | fsuppcor 9395 |
. . . 4
β’ (π β ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))) finSupp (0gβ((πΌ β π½) mPoly π
))) |
358 | 53, 290, 291, 293, 296, 304, 314, 357 | gsummhm 19800 |
. . 3
β’ (π β (π
Ξ£g ((π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) β ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))))) = ((π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½))))β(((πΌ β π½) mPoly π
) Ξ£g ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))))) |
359 | | fveq1 6887 |
. . . 4
β’ (π£ = (((πΌ β π½) mPoly π
) Ξ£g ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))) β (π£β(π βΎ (πΌ β π½))) = ((((πΌ β π½) mPoly π
) Ξ£g ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))))β(π βΎ (πΌ β π½)))) |
360 | 53, 290, 291, 296, 314, 357 | gsumcl 19777 |
. . . 4
β’ (π β (((πΌ β π½) mPoly π
) Ξ£g ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))) β (Baseβ((πΌ β π½) mPoly π
))) |
361 | | fvexd 6903 |
. . . 4
β’ (π β ((((πΌ β π½) mPoly π
) Ξ£g ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))))β(π βΎ (πΌ β π½))) β V) |
362 | 298, 359,
360, 361 | fvmptd3 7018 |
. . 3
β’ (π β ((π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½))))β(((πΌ β π½) mPoly π
) Ξ£g ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))))) = ((((πΌ β π½) mPoly π
) Ξ£g ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))))β(π βΎ (πΌ β π½)))) |
363 | 316 | ringcmnd 20094 |
. . . . . 6
β’ (π β (π½ mPoly ((πΌ β π½) mPoly π
)) β CMnd) |
364 | 351 | grpmndd 18828 |
. . . . . 6
β’ (π β ((πΌ β π½) mPoly π
) β Mnd) |
365 | 16, 317, 363, 364, 296, 354, 313, 349 | gsummhm 19800 |
. . . . 5
β’ (π β (((πΌ β π½) mPoly π
) Ξ£g ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))) = ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½)))β((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))))) |
366 | | fveq1 6887 |
. . . . . 6
β’ (π€ = ((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))) β (π€β(π βΎ π½)) = (((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))β(π βΎ π½))) |
367 | 16, 317, 363, 296, 313, 349 | gsumcl 19777 |
. . . . . 6
β’ (π β ((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
368 | | fvexd 6903 |
. . . . . 6
β’ (π β (((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))β(π βΎ π½)) β V) |
369 | 350, 366,
367, 368 | fvmptd3 7018 |
. . . . 5
β’ (π β ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½)))β((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))) = (((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))β(π βΎ π½))) |
370 | 365, 369 | eqtrd 2772 |
. . . 4
β’ (π β (((πΌ β π½) mPoly π
) Ξ£g ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))) = (((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))β(π βΎ π½))) |
371 | 370 | fveq1d 6890 |
. . 3
β’ (π β ((((πΌ β π½) mPoly π
) Ξ£g ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))))β(π βΎ (πΌ β π½))) = ((((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))β(π βΎ π½))β(π βΎ (πΌ β π½)))) |
372 | 358, 362,
371 | 3eqtrrd 2777 |
. 2
β’ (π β ((((π½ mPoly ((πΌ β π½) mPoly π
)) Ξ£g (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))β(π βΎ π½))β(π βΎ (πΌ β π½))) = (π
Ξ£g ((π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) β ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))))) |
373 | 4, 53, 16, 305, 312 | mplelf 21548 |
. . . . . . 7
β’ ((π β§ π β π·) β (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))):{π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β
Fin}βΆ(Baseβ((πΌ
β π½) mPoly π
))) |
374 | 308 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β π·) β (π βΎ π½) β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β
Fin}) |
375 | 373, 374 | ffvelcdmd 7084 |
. . . . . 6
β’ ((π β§ π β π·) β ((((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))β(π βΎ π½)) β (Baseβ((πΌ β π½) mPoly π
))) |
376 | | eqidd 2733 |
. . . . . . 7
β’ (π β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))) = (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))) |
377 | | eqidd 2733 |
. . . . . . 7
β’ (π β (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) = (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½)))) |
378 | | fveq1 6887 |
. . . . . . 7
β’ (π€ = (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))) β (π€β(π βΎ π½)) = ((((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))β(π βΎ π½))) |
379 | 312, 376,
377, 378 | fmptco 7123 |
. . . . . 6
β’ (π β ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))) = (π β π· β¦ ((((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))β(π βΎ π½)))) |
380 | | eqidd 2733 |
. . . . . 6
β’ (π β (π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) = (π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½))))) |
381 | | fveq1 6887 |
. . . . . 6
β’ (π£ = ((((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))β(π βΎ π½)) β (π£β(π βΎ (πΌ β π½))) = (((((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))β(π βΎ π½))β(π βΎ (πΌ β π½)))) |
382 | 375, 379,
380, 381 | fmptco 7123 |
. . . . 5
β’ (π β ((π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) β ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))) = (π β π· β¦ (((((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))β(π βΎ π½))β(π βΎ (πΌ β π½))))) |
383 | | eqid 2732 |
. . . . . . . . . 10
β’
(.rβ((πΌ β π½) mPoly π
)) = (.rβ((πΌ β π½) mPoly π
)) |
384 | 4, 249, 53, 16, 383, 305, 262, 281, 374 | mplvscaval 21566 |
. . . . . . . . 9
β’ ((π β§ π β π·) β ((((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))β(π βΎ π½)) = (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))(.rβ((πΌ β π½) mPoly π
))((((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))β(π βΎ π½)))) |
385 | 4, 249, 53, 16, 383, 305, 279, 248, 374 | mplvscaval 21566 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β ((((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))β(π βΎ π½)) = (((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½)))) |
386 | 385 | oveq2d 7421 |
. . . . . . . . 9
β’ ((π β§ π β π·) β (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))(.rβ((πΌ β π½) mPoly π
))((((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))β(π βΎ π½))) = (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½))))) |
387 | 30 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β ((πΌ β π½) mPoly π
) β AssAlg) |
388 | 35 | fveq2d 6892 |
. . . . . . . . . . . 12
β’ (π β (Baseβπ
) =
(Baseβ(Scalarβ((πΌ β π½) mPoly π
)))) |
389 | 388 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (Baseβπ
) = (Baseβ(Scalarβ((πΌ β π½) mPoly π
)))) |
390 | 74, 389 | eleqtrd 2835 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (πΉβπ) β (Baseβ(Scalarβ((πΌ β π½) mPoly π
)))) |
391 | 48 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β ((πΌ β π½) mPoly π
) β Ring) |
392 | 4, 53, 16, 305, 248 | mplelf 21548 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))):{π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β
Fin}βΆ(Baseβ((πΌ
β π½) mPoly π
))) |
393 | 392, 374 | ffvelcdmd 7084 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½)) β (Baseβ((πΌ β π½) mPoly π
))) |
394 | 53, 383, 391, 279, 393 | ringcld 20073 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½))) β (Baseβ((πΌ β π½) mPoly π
))) |
395 | | eqid 2732 |
. . . . . . . . . . 11
β’
(Baseβ(Scalarβ((πΌ β π½) mPoly π
))) = (Baseβ(Scalarβ((πΌ β π½) mPoly π
))) |
396 | | eqid 2732 |
. . . . . . . . . . 11
β’ (
Β·π β((πΌ β π½) mPoly π
)) = ( Β·π
β((πΌ β π½) mPoly π
)) |
397 | 31, 32, 395, 53, 383, 396 | asclmul1 21431 |
. . . . . . . . . 10
β’ ((((πΌ β π½) mPoly π
) β AssAlg β§ (πΉβπ) β (Baseβ(Scalarβ((πΌ β π½) mPoly π
))) β§ (((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½))) β (Baseβ((πΌ β π½) mPoly π
))) β (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½)))) = ((πΉβπ)( Β·π
β((πΌ β π½) mPoly π
))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½))))) |
398 | 387, 390,
394, 397 | syl3anc 1371 |
. . . . . . . . 9
β’ ((π β§ π β π·) β (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½)))) = ((πΉβπ)( Β·π
β((πΌ β π½) mPoly π
))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½))))) |
399 | 384, 386,
398 | 3eqtrd 2776 |
. . . . . . . 8
β’ ((π β§ π β π·) β ((((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))β(π βΎ π½)) = ((πΉβπ)( Β·π
β((πΌ β π½) mPoly π
))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½))))) |
400 | 399 | fveq1d 6890 |
. . . . . . 7
β’ ((π β§ π β π·) β (((((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))β(π βΎ π½))β(π βΎ (πΌ β π½))) = (((πΉβπ)( Β·π
β((πΌ β π½) mPoly π
))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½))))β(π βΎ (πΌ β π½)))) |
401 | | eqid 2732 |
. . . . . . . 8
β’
(.rβπ
) = (.rβπ
) |
402 | 301 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β π·) β (π βΎ (πΌ β π½)) β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β
Fin}) |
403 | 3, 396, 67, 53, 401, 297, 74, 394, 402 | mplvscaval 21566 |
. . . . . . 7
β’ ((π β§ π β π·) β (((πΉβπ)( Β·π
β((πΌ β π½) mPoly π
))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½))))β(π βΎ (πΌ β π½))) = ((πΉβπ)(.rβπ
)((((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½)))β(π βΎ (πΌ β π½))))) |
404 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’
(1rβπ
) = (1rβπ
) |
405 | 8 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β π
β CRing) |
406 | 15, 297, 83, 133, 70 | psrbagres 41112 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (π βΎ (πΌ β π½)) β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β
Fin}) |
407 | 3, 297, 331, 404, 203, 167, 169, 56, 405, 406 | mplcoe2 21587 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
))) = ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))) |
408 | 177 | fvresd 6908 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((π βΎ (πΌ β π½))βπ) = (πβπ)) |
409 | 408 | oveq1d 7420 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)) = ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))) |
410 | 409 | mpteq2dva 5247 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)))) |
411 | 410 | oveq2d 7421 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)))) = ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))) |
412 | 407, 411 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
))) = ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))) |
413 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’ (π β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β Fin} β¦
if(π = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
)))) = (π β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β Fin} β¦
if(π = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
)))) |
414 | | eqeq1 2736 |
. . . . . . . . . . . . . . 15
β’ (π = (π βΎ π½) β (π = (π βΎ π½) β (π βΎ π½) = (π βΎ π½))) |
415 | 414 | ifbid 4550 |
. . . . . . . . . . . . . 14
β’ (π = (π βΎ π½) β if(π = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))) = if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
)))) |
416 | | fvexd 6903 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (1rβ((πΌ β π½) mPoly π
)) β V) |
417 | | fvexd 6903 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (0gβ((πΌ β π½) mPoly π
)) β V) |
418 | 416, 417 | ifcld 4573 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))) β V) |
419 | 413, 415,
374, 418 | fvmptd3 7018 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β ((π β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β Fin} β¦
if(π = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))))β(π βΎ π½)) = if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
)))) |
420 | | eqid 2732 |
. . . . . . . . . . . . . . . 16
β’
(1rβ((πΌ β π½) mPoly π
)) = (1rβ((πΌ β π½) mPoly π
)) |
421 | 22 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β ((πΌ β π½) mPoly π
) β CRing) |
422 | 15, 305, 83, 147, 70 | psrbagres 41112 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β (π βΎ π½) β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β
Fin}) |
423 | 4, 305, 290, 420, 235, 17, 18, 47, 421, 422 | mplcoe2 21587 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (π β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β Fin} β¦
if(π = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
)))) = ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))) |
424 | | simpr 485 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π·) β§ π β π½) β π β π½) |
425 | 424 | fvresd 6908 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β π½) β ((π βΎ π½)βπ) = (πβπ)) |
426 | 425 | oveq1d 7420 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β π½) β (((π βΎ π½)βπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)) = ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))) |
427 | 426 | mpteq2dva 5247 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))) |
428 | 427 | oveq2d 7421 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))) = ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))) |
429 | 423, 428 | eqtrd 2772 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (π β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β Fin} β¦
if(π = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
)))) = ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))) |
430 | 429 | fveq1d 6890 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β ((π β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β Fin} β¦
if(π = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))))β(π βΎ π½)) = (((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½))) |
431 | 419, 430 | eqtr3d 2774 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))) = (((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½))) |
432 | 412, 431 | oveq12d 7423 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
)))) = (((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½)))) |
433 | 432 | eqcomd 2738 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½))) = ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))))) |
434 | 433 | fveq1d 6890 |
. . . . . . . . 9
β’ ((π β§ π β π·) β ((((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½)))β(π βΎ (πΌ β π½))) = (((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))))β(π βΎ (πΌ β π½)))) |
435 | 434 | oveq2d 7421 |
. . . . . . . 8
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)((((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½)))β(π βΎ (πΌ β π½)))) = ((πΉβπ)(.rβπ
)(((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))))β(π βΎ (πΌ β π½))))) |
436 | | ovif2 7503 |
. . . . . . . . . . . 12
β’ ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
)))) = if((π βΎ π½) = (π βΎ π½), ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(1rβ((πΌ β π½) mPoly π
))), ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(0gβ((πΌ β π½) mPoly π
)))) |
437 | 436 | fveq1i 6889 |
. . . . . . . . . . 11
β’ (((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))))β(π βΎ (πΌ β π½))) = (if((π βΎ π½) = (π βΎ π½), ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(1rβ((πΌ β π½) mPoly π
))), ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(0gβ((πΌ β π½) mPoly π
))))β(π βΎ (πΌ β π½))) |
438 | | iffv 6905 |
. . . . . . . . . . . 12
β’
(if((π βΎ π½) = (π βΎ π½), ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(1rβ((πΌ β π½) mPoly π
))), ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(0gβ((πΌ β π½) mPoly π
))))β(π βΎ (πΌ β π½))) = if((π βΎ π½) = (π βΎ π½), (((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(1rβ((πΌ β π½) mPoly π
)))β(π βΎ (πΌ β π½))), (((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(0gβ((πΌ β π½) mPoly π
)))β(π βΎ (πΌ β π½)))) |
439 | | eqeq1 2736 |
. . . . . . . . . . . . . . 15
β’ (π = (π βΎ (πΌ β π½)) β (π = (π βΎ (πΌ β π½)) β (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)))) |
440 | 439 | ifbid 4550 |
. . . . . . . . . . . . . 14
β’ (π = (π βΎ (πΌ β π½)) β if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)) = if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
))) |
441 | 57 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β π
β Ring) |
442 | 3, 53, 331, 404, 297, 203, 441, 406 | mplmon 21581 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
))) β (Baseβ((πΌ β π½) mPoly π
))) |
443 | 53, 383, 420, 391, 442 | ringridmd 20083 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(1rβ((πΌ β π½) mPoly π
))) = (π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))) |
444 | | fvexd 6903 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (1rβπ
) β V) |
445 | | fvexd 6903 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (0gβπ
) β V) |
446 | 444, 445 | ifcld 4573 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)) β V) |
447 | 440, 443,
402, 446 | fvmptd4 41050 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(1rβ((πΌ β π½) mPoly π
)))β(π βΎ (πΌ β π½))) = if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
))) |
448 | 53, 383, 290, 391, 442 | ringrzd 41083 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(0gβ((πΌ β π½) mPoly π
))) = (0gβ((πΌ β π½) mPoly π
))) |
449 | 448 | fveq1d 6890 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(0gβ((πΌ β π½) mPoly π
)))β(π βΎ (πΌ β π½))) = ((0gβ((πΌ β π½) mPoly π
))β(π βΎ (πΌ β π½)))) |
450 | 3, 297, 331, 290, 21, 292 | mpl0 21556 |
. . . . . . . . . . . . . . . 16
β’ (π β
(0gβ((πΌ
β π½) mPoly π
)) = ({π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} Γ
{(0gβπ
)})) |
451 | 450 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (0gβ((πΌ β π½) mPoly π
)) = ({π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} Γ
{(0gβπ
)})) |
452 | 451 | fveq1d 6890 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β ((0gβ((πΌ β π½) mPoly π
))β(π βΎ (πΌ β π½))) = (({π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} Γ
{(0gβπ
)})β(π βΎ (πΌ β π½)))) |
453 | | fvex 6901 |
. . . . . . . . . . . . . . . 16
β’
(0gβπ
) β V |
454 | 453 | fvconst2 7201 |
. . . . . . . . . . . . . . 15
β’ ((π βΎ (πΌ β π½)) β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β (({π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} Γ
{(0gβπ
)})β(π βΎ (πΌ β π½))) = (0gβπ
)) |
455 | 402, 454 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (({π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} Γ
{(0gβπ
)})β(π βΎ (πΌ β π½))) = (0gβπ
)) |
456 | 449, 452,
455 | 3eqtrd 2776 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(0gβ((πΌ β π½) mPoly π
)))β(π βΎ (πΌ β π½))) = (0gβπ
)) |
457 | 447, 456 | ifeq12d 4548 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β if((π βΎ π½) = (π βΎ π½), (((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(1rβ((πΌ β π½) mPoly π
)))β(π βΎ (πΌ β π½))), (((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(0gβ((πΌ β π½) mPoly π
)))β(π βΎ (πΌ β π½)))) = if((π βΎ π½) = (π βΎ π½), if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)), (0gβπ
))) |
458 | 438, 457 | eqtrid 2784 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (if((π βΎ π½) = (π βΎ π½), ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(1rβ((πΌ β π½) mPoly π
))), ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(0gβ((πΌ β π½) mPoly π
))))β(π βΎ (πΌ β π½))) = if((π βΎ π½) = (π βΎ π½), if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)), (0gβπ
))) |
459 | 437, 458 | eqtrid 2784 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))))β(π βΎ (πΌ β π½))) = if((π βΎ π½) = (π βΎ π½), if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)), (0gβπ
))) |
460 | 459 | oveq2d 7421 |
. . . . . . . . 9
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)(((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))))β(π βΎ (πΌ β π½)))) = ((πΉβπ)(.rβπ
)if((π βΎ π½) = (π βΎ π½), if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)), (0gβπ
)))) |
461 | | ifan 4580 |
. . . . . . . . . . 11
β’
if(((π βΎ π½) = (π βΎ π½) β§ (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½))), (1rβπ
), (0gβπ
)) = if((π βΎ π½) = (π βΎ π½), if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)), (0gβπ
)) |
462 | 461 | oveq2i 7416 |
. . . . . . . . . 10
β’ ((πΉβπ)(.rβπ
)if(((π βΎ π½) = (π βΎ π½) β§ (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½))), (1rβπ
), (0gβπ
))) = ((πΉβπ)(.rβπ
)if((π βΎ π½) = (π βΎ π½), if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)), (0gβπ
))) |
463 | 15 | psrbagf 21462 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π· β π:πΌβΆβ0) |
464 | 300, 463 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β π:πΌβΆβ0) |
465 | 464 | ffnd 6715 |
. . . . . . . . . . . . . . . 16
β’ (π β π Fn πΌ) |
466 | 465 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β π Fn πΌ) |
467 | | undif 4480 |
. . . . . . . . . . . . . . . . . 18
β’ (π½ β πΌ β (π½ βͺ (πΌ β π½)) = πΌ) |
468 | 9, 467 | sylib 217 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π½ βͺ (πΌ β π½)) = πΌ) |
469 | 468 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β (π½ βͺ (πΌ β π½)) = πΌ) |
470 | 469 | fneq2d 6640 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (π Fn (π½ βͺ (πΌ β π½)) β π Fn πΌ)) |
471 | 466, 470 | mpbird 256 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β π Fn (π½ βͺ (πΌ β π½))) |
472 | 87 | ffnd 6715 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β π Fn πΌ) |
473 | 469 | fneq2d 6640 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (π Fn (π½ βͺ (πΌ β π½)) β π Fn πΌ)) |
474 | 472, 473 | mpbird 256 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β π Fn (π½ βͺ (πΌ β π½))) |
475 | | eqfnun 7035 |
. . . . . . . . . . . . . 14
β’ ((π Fn (π½ βͺ (πΌ β π½)) β§ π Fn (π½ βͺ (πΌ β π½))) β (π = π β ((π βΎ π½) = (π βΎ π½) β§ (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½))))) |
476 | 471, 474,
475 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (π = π β ((π βΎ π½) = (π βΎ π½) β§ (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½))))) |
477 | 476 | ifbid 4550 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β if(π = π, (1rβπ
), (0gβπ
)) = if(((π βΎ π½) = (π βΎ π½) β§ (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½))), (1rβπ
), (0gβπ
))) |
478 | 477 | oveq2d 7421 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)if(π = π, (1rβπ
), (0gβπ
))) = ((πΉβπ)(.rβπ
)if(((π βΎ π½) = (π βΎ π½) β§ (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½))), (1rβπ
), (0gβπ
)))) |
479 | | ovif2 7503 |
. . . . . . . . . . 11
β’ ((πΉβπ)(.rβπ
)if(π = π, (1rβπ
), (0gβπ
))) = if(π = π, ((πΉβπ)(.rβπ
)(1rβπ
)), ((πΉβπ)(.rβπ
)(0gβπ
))) |
480 | 478, 479 | eqtr3di 2787 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)if(((π βΎ π½) = (π βΎ π½) β§ (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½))), (1rβπ
), (0gβπ
))) = if(π = π, ((πΉβπ)(.rβπ
)(1rβπ
)), ((πΉβπ)(.rβπ
)(0gβπ
)))) |
481 | 462, 480 | eqtr3id 2786 |
. . . . . . . . 9
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)if((π βΎ π½) = (π βΎ π½), if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)), (0gβπ
))) = if(π = π, ((πΉβπ)(.rβπ
)(1rβπ
)), ((πΉβπ)(.rβπ
)(0gβπ
)))) |
482 | 460, 481 | eqtrd 2772 |
. . . . . . . 8
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)(((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))))β(π βΎ (πΌ β π½)))) = if(π = π, ((πΉβπ)(.rβπ
)(1rβπ
)), ((πΉβπ)(.rβπ
)(0gβπ
)))) |
483 | 67, 401, 404, 441, 74 | ringridmd 20083 |
. . . . . . . . 9
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)(1rβπ
)) = (πΉβπ)) |
484 | 67, 401, 331, 441, 74 | ringrzd 41083 |
. . . . . . . . 9
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)(0gβπ
)) = (0gβπ
)) |
485 | 483, 484 | ifeq12d 4548 |
. . . . . . . 8
β’ ((π β§ π β π·) β if(π = π, ((πΉβπ)(.rβπ
)(1rβπ
)), ((πΉβπ)(.rβπ
)(0gβπ
))) = if(π = π, (πΉβπ), (0gβπ
))) |
486 | 435, 482,
485 | 3eqtrd 2776 |
. . . . . . 7
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)((((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½)))β(π βΎ (πΌ β π½)))) = if(π = π, (πΉβπ), (0gβπ
))) |
487 | 400, 403,
486 | 3eqtrd 2776 |
. . . . . 6
β’ ((π β§ π β π·) β (((((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))β(π βΎ π½))β(π βΎ (πΌ β π½))) = if(π = π, (πΉβπ), (0gβπ
))) |
488 | 487 | mpteq2dva 5247 |
. . . . 5
β’ (π β (π β π· β¦ (((((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))β(π βΎ π½))β(π βΎ (πΌ β π½)))) = (π β π· β¦ if(π = π, (πΉβπ), (0gβπ
)))) |
489 | 382, 488 | eqtrd 2772 |
. . . 4
β’ (π β ((π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) β ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))))))) = (π β π· β¦ if(π = π, (πΉβπ), (0gβπ
)))) |
490 | 489 | oveq2d 7421 |
. . 3
β’ (π β (π
Ξ£g ((π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) β ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))))) = (π
Ξ£g (π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))))) |
491 | 57 | ringcmnd 20094 |
. . . 4
β’ (π β π
β CMnd) |
492 | 67, 331 | ring0cl 20077 |
. . . . . . . 8
β’ (π
β Ring β
(0gβπ
)
β (Baseβπ
)) |
493 | 57, 492 | syl 17 |
. . . . . . 7
β’ (π β (0gβπ
) β (Baseβπ
)) |
494 | 493 | adantr 481 |
. . . . . 6
β’ ((π β§ π β π·) β (0gβπ
) β (Baseβπ
)) |
495 | 74, 494 | ifcld 4573 |
. . . . 5
β’ ((π β§ π β π·) β if(π = π, (πΉβπ), (0gβπ
)) β (Baseβπ
)) |
496 | 495 | fmpttd 7111 |
. . . 4
β’ (π β (π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))):π·βΆ(Baseβπ
)) |
497 | | eldifsnneq 4793 |
. . . . . . . 8
β’ (π β (π· β {π}) β Β¬ π = π) |
498 | 497 | neqcomd 2742 |
. . . . . . 7
β’ (π β (π· β {π}) β Β¬ π = π) |
499 | 498 | iffalsed 4538 |
. . . . . 6
β’ (π β (π· β {π}) β if(π = π, (πΉβπ), (0gβπ
)) = (0gβπ
)) |
500 | 499 | adantl 482 |
. . . . 5
β’ ((π β§ π β (π· β {π})) β if(π = π, (πΉβπ), (0gβπ
)) = (0gβπ
)) |
501 | 500, 296 | suppss2 8181 |
. . . 4
β’ (π β ((π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) supp (0gβπ
)) β {π}) |
502 | 296 | mptexd 7222 |
. . . . 5
β’ (π β (π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) β V) |
503 | | funmpt 6583 |
. . . . . 6
β’ Fun
(π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) |
504 | 503 | a1i 11 |
. . . . 5
β’ (π β Fun (π β π· β¦ if(π = π, (πΉβπ), (0gβπ
)))) |
505 | | snfi 9040 |
. . . . . . 7
β’ {π} β Fin |
506 | 505 | a1i 11 |
. . . . . 6
β’ (π β {π} β Fin) |
507 | 506, 501 | ssfid 9263 |
. . . . 5
β’ (π β ((π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) supp (0gβπ
)) β Fin) |
508 | 502, 493,
504, 507 | isfsuppd 9362 |
. . . 4
β’ (π β (π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) finSupp (0gβπ
)) |
509 | 67, 331, 491, 296, 496, 501, 508 | gsumres 19775 |
. . 3
β’ (π β (π
Ξ£g ((π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) βΎ {π})) = (π
Ξ£g (π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))))) |
510 | 300 | snssd 4811 |
. . . . . 6
β’ (π β {π} β π·) |
511 | 510 | resmptd 6038 |
. . . . 5
β’ (π β ((π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) βΎ {π}) = (π β {π} β¦ if(π = π, (πΉβπ), (0gβπ
)))) |
512 | 511 | oveq2d 7421 |
. . . 4
β’ (π β (π
Ξ£g ((π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) βΎ {π})) = (π
Ξ£g (π β {π} β¦ if(π = π, (πΉβπ), (0gβπ
))))) |
513 | 68, 300 | ffvelcdmd 7084 |
. . . . 5
β’ (π β (πΉβπ) β (Baseβπ
)) |
514 | | iftrue 4533 |
. . . . . . . 8
β’ (π = π β if(π = π, (πΉβπ), (0gβπ
)) = (πΉβπ)) |
515 | | fveq2 6888 |
. . . . . . . . 9
β’ (π = π β (πΉβπ) = (πΉβπ)) |
516 | 515 | eqcoms 2740 |
. . . . . . . 8
β’ (π = π β (πΉβπ) = (πΉβπ)) |
517 | 514, 516 | eqtrd 2772 |
. . . . . . 7
β’ (π = π β if(π = π, (πΉβπ), (0gβπ
)) = (πΉβπ)) |
518 | 517 | eqcoms 2740 |
. . . . . 6
β’ (π = π β if(π = π, (πΉβπ), (0gβπ
)) = (πΉβπ)) |
519 | 67, 518 | gsumsn 19816 |
. . . . 5
β’ ((π
β Mnd β§ π β π· β§ (πΉβπ) β (Baseβπ
)) β (π
Ξ£g (π β {π} β¦ if(π = π, (πΉβπ), (0gβπ
)))) = (πΉβπ)) |
520 | 293, 300,
513, 519 | syl3anc 1371 |
. . . 4
β’ (π β (π
Ξ£g (π β {π} β¦ if(π = π, (πΉβπ), (0gβπ
)))) = (πΉβπ)) |
521 | 512, 520 | eqtrd 2772 |
. . 3
β’ (π β (π
Ξ£g ((π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) βΎ {π})) = (πΉβπ)) |
522 | 490, 509,
521 | 3eqtr2d 2778 |
. 2
β’ (π β (π
Ξ£g ((π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) β ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β (π β π· β¦ (((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))(((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))))))) = (πΉβπ)) |
523 | 289, 372,
522 | 3eqtrd 2776 |
1
β’ (π β (((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½))) = (πΉβπ)) |