Step | Hyp | Ref
| Expression |
1 | | selvvvval.p |
. . . . . 6
β’ π = (πΌ mPoly π
) |
2 | | selvvvval.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
3 | | eqid 2725 |
. . . . . 6
β’ ((πΌ β π½) mPoly π
) = ((πΌ β π½) mPoly π
) |
4 | | eqid 2725 |
. . . . . 6
β’ (π½ mPoly ((πΌ β π½) mPoly π
)) = (π½ mPoly ((πΌ β π½) mPoly π
)) |
5 | | eqid 2725 |
. . . . . 6
β’
(algScβ(π½
mPoly ((πΌ β π½) mPoly π
))) = (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) |
6 | | eqid 2725 |
. . . . . 6
β’
((algScβ(π½
mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) |
7 | | selvvvval.r |
. . . . . 6
β’ (π β π
β CRing) |
8 | | selvvvval.j |
. . . . . 6
β’ (π β π½ β πΌ) |
9 | | selvvvval.f |
. . . . . 6
β’ (π β πΉ β π΅) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | selvval2 41882 |
. . . . 5
β’ (π β (((πΌ selectVars π
)βπ½)βπΉ) = (((πΌ eval (π½ mPoly ((πΌ β π½) mPoly π
)))β(((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β πΉ))β(π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)))))) |
11 | | eqid 2725 |
. . . . . 6
β’ (πΌ eval (π½ mPoly ((πΌ β π½) mPoly π
))) = (πΌ eval (π½ mPoly ((πΌ β π½) mPoly π
))) |
12 | | eqid 2725 |
. . . . . 6
β’ (πΌ mPoly (π½ mPoly ((πΌ β π½) mPoly π
))) = (πΌ mPoly (π½ mPoly ((πΌ β π½) mPoly π
))) |
13 | | eqid 2725 |
. . . . . 6
β’
(Baseβ(πΌ mPoly
(π½ mPoly ((πΌ β π½) mPoly π
)))) = (Baseβ(πΌ mPoly (π½ mPoly ((πΌ β π½) mPoly π
)))) |
14 | | selvvvval.d |
. . . . . 6
β’ π· = {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
15 | | eqid 2725 |
. . . . . 6
β’
(Baseβ(π½ mPoly
((πΌ β π½) mPoly π
))) = (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) |
16 | | eqid 2725 |
. . . . . 6
β’
(mulGrpβ(π½
mPoly ((πΌ β π½) mPoly π
))) = (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) |
17 | | eqid 2725 |
. . . . . 6
β’
(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
)))) =
(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
18 | | eqid 2725 |
. . . . . 6
β’
(.rβ(π½ mPoly ((πΌ β π½) mPoly π
))) = (.rβ(π½ mPoly ((πΌ β π½) mPoly π
))) |
19 | 1, 2 | mplrcl 21943 |
. . . . . . 7
β’ (πΉ β π΅ β πΌ β V) |
20 | 9, 19 | syl 17 |
. . . . . 6
β’ (π β πΌ β V) |
21 | 20, 8 | ssexd 5319 |
. . . . . . 7
β’ (π β π½ β V) |
22 | 20 | difexd 5326 |
. . . . . . . 8
β’ (π β (πΌ β π½) β V) |
23 | 3, 22, 7 | mplcrngd 41835 |
. . . . . . 7
β’ (π β ((πΌ β π½) mPoly π
) β CRing) |
24 | 4, 21, 23 | mplcrngd 41835 |
. . . . . 6
β’ (π β (π½ mPoly ((πΌ β π½) mPoly π
)) β CRing) |
25 | 4 | mplassa 21971 |
. . . . . . . . . . 11
β’ ((π½ β V β§ ((πΌ β π½) mPoly π
) β CRing) β (π½ mPoly ((πΌ β π½) mPoly π
)) β AssAlg) |
26 | 21, 23, 25 | syl2anc 582 |
. . . . . . . . . 10
β’ (π β (π½ mPoly ((πΌ β π½) mPoly π
)) β AssAlg) |
27 | | eqid 2725 |
. . . . . . . . . . 11
β’
(Scalarβ(π½
mPoly ((πΌ β π½) mPoly π
))) = (Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))) |
28 | 5, 27 | asclrhm 21827 |
. . . . . . . . . 10
β’ ((π½ mPoly ((πΌ β π½) mPoly π
)) β AssAlg β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β ((Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))) RingHom (π½ mPoly ((πΌ β π½) mPoly π
)))) |
29 | 26, 28 | syl 17 |
. . . . . . . . 9
β’ (π β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β ((Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))) RingHom (π½ mPoly ((πΌ β π½) mPoly π
)))) |
30 | 3 | mplassa 21971 |
. . . . . . . . . . . 12
β’ (((πΌ β π½) β V β§ π
β CRing) β ((πΌ β π½) mPoly π
) β AssAlg) |
31 | 22, 7, 30 | syl2anc 582 |
. . . . . . . . . . 11
β’ (π β ((πΌ β π½) mPoly π
) β AssAlg) |
32 | | eqid 2725 |
. . . . . . . . . . . 12
β’
(algScβ((πΌ
β π½) mPoly π
)) = (algScβ((πΌ β π½) mPoly π
)) |
33 | | eqid 2725 |
. . . . . . . . . . . 12
β’
(Scalarβ((πΌ
β π½) mPoly π
)) = (Scalarβ((πΌ β π½) mPoly π
)) |
34 | 32, 33 | asclrhm 21827 |
. . . . . . . . . . 11
β’ (((πΌ β π½) mPoly π
) β AssAlg β (algScβ((πΌ β π½) mPoly π
)) β ((Scalarβ((πΌ β π½) mPoly π
)) RingHom ((πΌ β π½) mPoly π
))) |
35 | 31, 34 | syl 17 |
. . . . . . . . . 10
β’ (π β (algScβ((πΌ β π½) mPoly π
)) β ((Scalarβ((πΌ β π½) mPoly π
)) RingHom ((πΌ β π½) mPoly π
))) |
36 | 3, 22, 7 | mplsca 21962 |
. . . . . . . . . . . 12
β’ (π β π
= (Scalarβ((πΌ β π½) mPoly π
))) |
37 | 36 | eqcomd 2731 |
. . . . . . . . . . 11
β’ (π β (Scalarβ((πΌ β π½) mPoly π
)) = π
) |
38 | 4, 21, 23 | mplsca 21962 |
. . . . . . . . . . 11
β’ (π β ((πΌ β π½) mPoly π
) = (Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
39 | 37, 38 | oveq12d 7434 |
. . . . . . . . . 10
β’ (π β ((Scalarβ((πΌ β π½) mPoly π
)) RingHom ((πΌ β π½) mPoly π
)) = (π
RingHom (Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
40 | 35, 39 | eleqtrd 2827 |
. . . . . . . . 9
β’ (π β (algScβ((πΌ β π½) mPoly π
)) β (π
RingHom (Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
41 | | rhmco 20444 |
. . . . . . . . 9
β’
(((algScβ(π½
mPoly ((πΌ β π½) mPoly π
))) β ((Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))) RingHom (π½ mPoly ((πΌ β π½) mPoly π
))) β§ (algScβ((πΌ β π½) mPoly π
)) β (π
RingHom (Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β (π
RingHom (π½ mPoly ((πΌ β π½) mPoly π
)))) |
42 | 29, 40, 41 | syl2anc 582 |
. . . . . . . 8
β’ (π β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β (π
RingHom (π½ mPoly ((πΌ β π½) mPoly π
)))) |
43 | | rhmghm 20427 |
. . . . . . . 8
β’
(((algScβ(π½
mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β (π
RingHom (π½ mPoly ((πΌ β π½) mPoly π
))) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β (π
GrpHom (π½ mPoly ((πΌ β π½) mPoly π
)))) |
44 | | ghmmhm 19184 |
. . . . . . . 8
β’
(((algScβ(π½
mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β (π
GrpHom (π½ mPoly ((πΌ β π½) mPoly π
))) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β (π
MndHom (π½ mPoly ((πΌ β π½) mPoly π
)))) |
45 | 42, 43, 44 | 3syl 18 |
. . . . . . 7
β’ (π β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β (π
MndHom (π½ mPoly ((πΌ β π½) mPoly π
)))) |
46 | 1, 12, 2, 13, 45, 9 | mhmcompl 41841 |
. . . . . 6
β’ (π β (((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β πΉ) β (Baseβ(πΌ mPoly (π½ mPoly ((πΌ β π½) mPoly π
))))) |
47 | | fvexd 6907 |
. . . . . . 7
β’ (π β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β V) |
48 | | eqid 2725 |
. . . . . . . . . . . 12
β’ (π½ mVar ((πΌ β π½) mPoly π
)) = (π½ mVar ((πΌ β π½) mPoly π
)) |
49 | 23 | crngringd 20190 |
. . . . . . . . . . . 12
β’ (π β ((πΌ β π½) mPoly π
) β Ring) |
50 | 4, 48, 15, 21, 49 | mvrf2 21942 |
. . . . . . . . . . 11
β’ (π β (π½ mVar ((πΌ β π½) mPoly π
)):π½βΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
51 | 50 | ffvelcdmda 7089 |
. . . . . . . . . 10
β’ ((π β§ π§ β π½) β ((π½ mVar ((πΌ β π½) mPoly π
))βπ§) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
52 | 51 | adantlr 713 |
. . . . . . . . 9
β’ (((π β§ π§ β πΌ) β§ π§ β π½) β ((π½ mVar ((πΌ β π½) mPoly π
))βπ§) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
53 | | eldif 3949 |
. . . . . . . . . . 11
β’ (π§ β (πΌ β π½) β (π§ β πΌ β§ Β¬ π§ β π½)) |
54 | | eqid 2725 |
. . . . . . . . . . . . . 14
β’
(Baseβ((πΌ
β π½) mPoly π
)) = (Baseβ((πΌ β π½) mPoly π
)) |
55 | 4, 15, 54, 5, 21, 49 | mplasclf 22016 |
. . . . . . . . . . . . 13
β’ (π β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))):(Baseβ((πΌ β π½) mPoly π
))βΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
56 | 55 | adantr 479 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (πΌ β π½)) β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))):(Baseβ((πΌ β π½) mPoly π
))βΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
57 | | eqid 2725 |
. . . . . . . . . . . . . 14
β’ ((πΌ β π½) mVar π
) = ((πΌ β π½) mVar π
) |
58 | 7 | crngringd 20190 |
. . . . . . . . . . . . . 14
β’ (π β π
β Ring) |
59 | 3, 57, 54, 22, 58 | mvrf2 21942 |
. . . . . . . . . . . . 13
β’ (π β ((πΌ β π½) mVar π
):(πΌ β π½)βΆ(Baseβ((πΌ β π½) mPoly π
))) |
60 | 59 | ffvelcdmda 7089 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (πΌ β π½)) β (((πΌ β π½) mVar π
)βπ§) β (Baseβ((πΌ β π½) mPoly π
))) |
61 | 56, 60 | ffvelcdmd 7090 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (πΌ β π½)) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
62 | 53, 61 | sylan2br 593 |
. . . . . . . . . 10
β’ ((π β§ (π§ β πΌ β§ Β¬ π§ β π½)) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
63 | 62 | anassrs 466 |
. . . . . . . . 9
β’ (((π β§ π§ β πΌ) β§ Β¬ π§ β π½) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
64 | 52, 63 | ifclda 4559 |
. . . . . . . 8
β’ ((π β§ π§ β πΌ) β if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
65 | 64 | fmpttd 7120 |
. . . . . . 7
β’ (π β (π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)))):πΌβΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
66 | 47, 20, 65 | elmapdd 8858 |
. . . . . 6
β’ (π β (π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)))) β ((Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) βm πΌ)) |
67 | 11, 12, 13, 14, 15, 16, 17, 18, 20, 24, 46, 66 | evlvvval 41871 |
. . . . 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 π
)βπ§))))βπ)))))))) |
68 | | eqid 2725 |
. . . . . . . . . . . . 13
β’
(Baseβπ
) =
(Baseβπ
) |
69 | 1, 68, 2, 14, 9 | mplelf 21947 |
. . . . . . . . . . . 12
β’ (π β πΉ:π·βΆ(Baseβπ
)) |
70 | 69 | adantr 479 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β πΉ:π·βΆ(Baseβπ
)) |
71 | | simpr 483 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β π β π·) |
72 | 70, 71 | fvco3d 6993 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β ((((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β πΉ)βπ) = (((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
)))β(πΉβπ))) |
73 | 3, 54, 68, 32, 22, 58 | mplasclf 22016 |
. . . . . . . . . . . 12
β’ (π β (algScβ((πΌ β π½) mPoly π
)):(Baseβπ
)βΆ(Baseβ((πΌ β π½) mPoly π
))) |
74 | 73 | adantr 479 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (algScβ((πΌ β π½) mPoly π
)):(Baseβπ
)βΆ(Baseβ((πΌ β π½) mPoly π
))) |
75 | 69 | ffvelcdmda 7089 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (πΉβπ) β (Baseβπ
)) |
76 | 74, 75 | fvco3d 6993 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
)))β(πΉβπ)) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)))) |
77 | 72, 76 | eqtrd 2765 |
. . . . . . . . 9
β’ ((π β§ π β π·) β ((((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ((πΌ β π½) mPoly π
))) β πΉ)βπ) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)))) |
78 | 16, 15 | mgpbas 20084 |
. . . . . . . . . . 11
β’
(Baseβ(π½ mPoly
((πΌ β π½) mPoly π
))) = (Baseβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
79 | | eqid 2725 |
. . . . . . . . . . 11
β’
(0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
)))) =
(0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
80 | 16, 18 | mgpplusg 20082 |
. . . . . . . . . . 11
β’
(.rβ(π½ mPoly ((πΌ β π½) mPoly π
))) =
(+gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
81 | 16 | crngmgp 20185 |
. . . . . . . . . . . . 13
β’ ((π½ mPoly ((πΌ β π½) mPoly π
)) β CRing β (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) β CMnd) |
82 | 24, 81 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) β CMnd) |
83 | 82 | adantr 479 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) β CMnd) |
84 | 20 | adantr 479 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β πΌ β V) |
85 | 82 | cmnmndd 19763 |
. . . . . . . . . . . . . 14
β’ (π β (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) β Mnd) |
86 | 85 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π β πΌ) β (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) β Mnd) |
87 | 14 | psrbagf 21855 |
. . . . . . . . . . . . . . 15
β’ (π β π· β π:πΌβΆβ0) |
88 | 87 | adantl 480 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β π:πΌβΆβ0) |
89 | 88 | ffvelcdmda 7089 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π β πΌ) β (πβπ) β
β0) |
90 | | eqid 2725 |
. . . . . . . . . . . . . . 15
β’ (π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)))) = (π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)))) |
91 | | eleq1w 2808 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π β (π§ β π½ β π β π½)) |
92 | | fveq2 6892 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π β ((π½ mVar ((πΌ β π½) mPoly π
))βπ§) = ((π½ mVar ((πΌ β π½) mPoly π
))βπ)) |
93 | | fveq2 6892 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π β (((πΌ β π½) mVar π
)βπ§) = (((πΌ β π½) mVar π
)βπ)) |
94 | 93 | fveq2d 6896 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§)) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) |
95 | 91, 92, 94 | ifbieq12d 4552 |
. . . . . . . . . . . . . . 15
β’ (π§ = π β if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))) = if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))) |
96 | | simpr 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β πΌ) β π β πΌ) |
97 | 50 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β πΌ) β (π½ mVar ((πΌ β π½) mPoly π
)):π½βΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
98 | 97 | ffvelcdmda 7089 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π·) β§ π β πΌ) β§ π β π½) β ((π½ mVar ((πΌ β π½) mPoly π
))βπ) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
99 | | eldif 3949 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πΌ β π½) β (π β πΌ β§ Β¬ π β π½)) |
100 | 55 | adantr 479 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (πΌ β π½)) β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))):(Baseβ((πΌ β π½) mPoly π
))βΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
101 | 59 | ffvelcdmda 7089 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (πΌ β π½)) β (((πΌ β π½) mVar π
)βπ) β (Baseβ((πΌ β π½) mPoly π
))) |
102 | 100, 101 | ffvelcdmd 7090 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (πΌ β π½)) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
103 | 99, 102 | sylan2br 593 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β πΌ β§ Β¬ π β π½)) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
104 | 103 | anassrs 466 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β πΌ) β§ Β¬ π β π½) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
105 | 104 | adantllr 717 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π·) β§ π β πΌ) β§ Β¬ π β π½) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
106 | 98, 105 | ifclda 4559 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β πΌ) β if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
107 | 90, 95, 96, 106 | fvmptd3 7023 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β πΌ) β ((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ) = if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))) |
108 | 107, 106 | eqeltrd 2825 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π β πΌ) β ((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
109 | 78, 17, 86, 89, 108 | mulgnn0cld 19054 |
. . . . . . . . . . . 12
β’ (((π β§ π β π·) β§ π β πΌ) β ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
110 | 109 | fmpttd 7120 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))):πΌβΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
111 | 88 | feqmptd 6962 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β π = (π β πΌ β¦ (πβπ))) |
112 | 14 | psrbagfsupp 21857 |
. . . . . . . . . . . . . 14
β’ (π β π· β π finSupp 0) |
113 | 112 | adantl 480 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β π finSupp 0) |
114 | 111, 113 | eqbrtrrd 5167 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (π β πΌ β¦ (πβπ)) finSupp 0) |
115 | 78, 79, 17 | mulg0 19034 |
. . . . . . . . . . . . 13
β’ (π‘ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β
(0(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))π‘) = (0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
116 | 115 | adantl 480 |
. . . . . . . . . . . 12
β’ (((π β§ π β π·) β§ π‘ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β
(0(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))π‘) = (0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
117 | | fvexd 6907 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β
(0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β V) |
118 | 114, 116,
89, 108, 117 | fsuppssov1 9407 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) finSupp
(0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
119 | | disjdifr 4468 |
. . . . . . . . . . . 12
β’ ((πΌ β π½) β© π½) = β
|
120 | 119 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β ((πΌ β π½) β© π½) = β
) |
121 | | undifr 4478 |
. . . . . . . . . . . . . 14
β’ (π½ β πΌ β ((πΌ β π½) βͺ π½) = πΌ) |
122 | 8, 121 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π β ((πΌ β π½) βͺ π½) = πΌ) |
123 | 122 | eqcomd 2731 |
. . . . . . . . . . . 12
β’ (π β πΌ = ((πΌ β π½) βͺ π½)) |
124 | 123 | adantr 479 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β πΌ = ((πΌ β π½) βͺ π½)) |
125 | 78, 79, 80, 83, 84, 110, 118, 120, 124 | gsumsplit 19887 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β ((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 π
)βπ§))))βπ))) βΎ π½)))) |
126 | | eldifi 4119 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πΌ β π½) β π β πΌ) |
127 | 126 | adantl 480 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β π β πΌ) |
128 | 126, 106 | sylan2 591 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
129 | 90, 95, 127, 128 | fvmptd3 7023 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ) = if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))) |
130 | | eldifn 4120 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πΌ β π½) β Β¬ π β π½) |
131 | 130 | adantl 480 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β Β¬ π β π½) |
132 | 131 | iffalsed 4535 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) |
133 | 129, 132 | eqtrd 2765 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) |
134 | 133 | oveq2d 7432 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)) = ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))) |
135 | | eqid 2725 |
. . . . . . . . . . . . . . . . . . . 20
β’
(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) = (mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
136 | 135, 16 | rhmmhm 20422 |
. . . . . . . . . . . . . . . . . . 19
β’
((algScβ(π½
mPoly ((πΌ β π½) mPoly π
))) β ((Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))) RingHom (π½ mPoly ((πΌ β π½) mPoly π
))) β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β
((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) MndHom (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
137 | 29, 136 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β
((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) MndHom (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
138 | 137 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β
((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) MndHom (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
139 | 126, 89 | sylan2 591 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (πβπ) β
β0) |
140 | 101 | adantlr 713 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (((πΌ β π½) mVar π
)βπ) β (Baseβ((πΌ β π½) mPoly π
))) |
141 | 38 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (Baseβ((πΌ β π½) mPoly π
)) = (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
142 | 141 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (Baseβ((πΌ β π½) mPoly π
)) = (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
143 | 140, 142 | eleqtrd 2827 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (((πΌ β π½) mVar π
)βπ) β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
144 | | eqid 2725 |
. . . . . . . . . . . . . . . . . . 19
β’
(Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) = (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
145 | 135, 144 | mgpbas 20084 |
. . . . . . . . . . . . . . . . . 18
β’
(Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) =
(Baseβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
146 | | eqid 2725 |
. . . . . . . . . . . . . . . . . 18
β’
(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) =
(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
147 | 145, 146,
17 | mhmmulg 19074 |
. . . . . . . . . . . . . . . . 17
β’
(((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 π
)βπ)))) |
148 | 138, 139,
143, 147 | syl3anc 1368 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))) = ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))) |
149 | 134, 148 | eqtr4d 2768 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))) |
150 | 149 | mpteq2dva 5243 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) = (π β (πΌ β π½) β¦ ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))))) |
151 | | difssd 4125 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (πΌ β π½) β πΌ) |
152 | 151 | resmptd 6039 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ (πΌ β π½)) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)))) |
153 | 55 | adantr 479 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))):(Baseβ((πΌ β π½) mPoly π
))βΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
154 | 38 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (mulGrpβ((πΌ β π½) mPoly π
)) = (mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
155 | 154 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(.gβ(mulGrpβ((πΌ β π½) mPoly π
))) =
(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))) |
156 | 155 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β
(.gβ(mulGrpβ((πΌ β π½) mPoly π
))) =
(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))) |
157 | 156 | oveqd 7433 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)) = ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))) |
158 | | eqid 2725 |
. . . . . . . . . . . . . . . . . 18
β’
(mulGrpβ((πΌ
β π½) mPoly π
)) = (mulGrpβ((πΌ β π½) mPoly π
)) |
159 | 158, 54 | mgpbas 20084 |
. . . . . . . . . . . . . . . . 17
β’
(Baseβ((πΌ
β π½) mPoly π
)) =
(Baseβ(mulGrpβ((πΌ β π½) mPoly π
))) |
160 | | eqid 2725 |
. . . . . . . . . . . . . . . . 17
β’
(.gβ(mulGrpβ((πΌ β π½) mPoly π
))) =
(.gβ(mulGrpβ((πΌ β π½) mPoly π
))) |
161 | 158 | crngmgp 20185 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΌ β π½) mPoly π
) β CRing β (mulGrpβ((πΌ β π½) mPoly π
)) β CMnd) |
162 | 23, 161 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (mulGrpβ((πΌ β π½) mPoly π
)) β CMnd) |
163 | 162 | cmnmndd 19763 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (mulGrpβ((πΌ β π½) mPoly π
)) β Mnd) |
164 | 163 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (mulGrpβ((πΌ β π½) mPoly π
)) β Mnd) |
165 | 159, 160,
164, 139, 140 | mulgnn0cld 19054 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)) β (Baseβ((πΌ β π½) mPoly π
))) |
166 | 157, 165 | eqeltrrd 2826 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)) β (Baseβ((πΌ β π½) mPoly π
))) |
167 | 153, 166 | cofmpt 7137 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))) = (π β (πΌ β π½) β¦ ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))))) |
168 | 150, 152,
167 | 3eqtr4d 2775 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ (πΌ β π½)) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))))) |
169 | 168 | oveq2d 7432 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ (πΌ β π½))) = ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g
((algScβ(π½ mPoly
((πΌ β π½) mPoly π
))) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))))) |
170 | | eqid 2725 |
. . . . . . . . . . . . 13
β’
(0gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) =
(0gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
171 | 38, 23 | eqeltrrd 2826 |
. . . . . . . . . . . . . . 15
β’ (π β (Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))) β CRing) |
172 | 135 | crngmgp 20185 |
. . . . . . . . . . . . . . 15
β’
((Scalarβ(π½
mPoly ((πΌ β π½) mPoly π
))) β CRing β
(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β CMnd) |
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β
(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β CMnd) |
174 | 173 | adantr 479 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β CMnd) |
175 | 85 | adantr 479 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) β Mnd) |
176 | 22 | adantr 479 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (πΌ β π½) β V) |
177 | 137 | adantr 479 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (algScβ(π½ mPoly ((πΌ β π½) mPoly π
))) β
((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) MndHom (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
178 | 166, 142 | eleqtrd 2827 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)) β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
179 | 178 | fmpttd 7120 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))):(πΌ β π½)βΆ(Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
180 | | 0zd 12600 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β 0 β β€) |
181 | 114, 151,
180 | fmptssfisupp 9417 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ (πβπ)) finSupp 0) |
182 | 141 | eqimssd 4029 |
. . . . . . . . . . . . . . . . 17
β’ (π β (Baseβ((πΌ β π½) mPoly π
)) β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
183 | 182 | sselda 3972 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (Baseβ((πΌ β π½) mPoly π
))) β π’ β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
184 | 183 | adantlr 713 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π’ β (Baseβ((πΌ β π½) mPoly π
))) β π’ β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
185 | 145, 170,
146 | mulg0 19034 |
. . . . . . . . . . . . . . 15
β’ (π’ β
(Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β
(0(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))π’) =
(0gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π’ β (Baseβ((πΌ β π½) mPoly π
))) β
(0(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))π’) =
(0gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))) |
187 | | fvexd 6907 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β
(0gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) β V) |
188 | 181, 186,
139, 140, 187 | fsuppssov1 9407 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))) finSupp
(0gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))) |
189 | 145, 170,
174, 175, 176, 177, 179, 188 | gsummhm 19897 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β ((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 π
)βπ)))))) |
190 | 169, 189 | eqtrd 2765 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ (πΌ β π½))) = ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))))) |
191 | 8 | adantr 479 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β π½ β πΌ) |
192 | 191 | resmptd 6039 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ π½) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)))) |
193 | 191 | sselda 3972 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β π½) β π β πΌ) |
194 | 193, 106 | syldan 589 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β π½) β if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
195 | 90, 95, 193, 194 | fvmptd3 7023 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β π½) β ((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ) = if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ)))) |
196 | | iftrue 4530 |
. . . . . . . . . . . . . . . . 17
β’ (π β π½ β if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) = ((π½ mVar ((πΌ β π½) mPoly π
))βπ)) |
197 | 196 | adantl 480 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β π½) β if(π β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ))) = ((π½ mVar ((πΌ β π½) mPoly π
))βπ)) |
198 | 195, 197 | eqtrd 2765 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β π½) β ((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ) = ((π½ mVar ((πΌ β π½) mPoly π
))βπ)) |
199 | 198 | oveq2d 7432 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β π½) β ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ)) = ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))) |
200 | 199 | mpteq2dva 5243 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))) |
201 | 192, 200 | eqtrd 2765 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π§ β πΌ β¦ if(π§ β π½, ((π½ mVar ((πΌ β π½) mPoly π
))βπ§), ((algScβ(π½ mPoly ((πΌ β π½) mPoly π
)))β(((πΌ β π½) mVar π
)βπ§))))βπ))) βΎ π½) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))) |
202 | 201 | oveq2d 7432 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β ((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 π
))βπ))))) |
203 | 190, 202 | oveq12d 7434 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (((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 π
)βπ§))))βπ))) βΎ π½))) = (((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 π
))βπ)))))) |
204 | 26 | adantr 479 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (π½ mPoly ((πΌ β π½) mPoly π
)) β AssAlg) |
205 | 145, 170,
174, 176, 179, 188 | gsumcl 19874 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β ((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))) β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
206 | 21 | adantr 479 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β π½ β V) |
207 | 85 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β π½) β (mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) β Mnd) |
208 | 193, 89 | syldan 589 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β π½) β (πβπ) β
β0) |
209 | 50 | ffvelcdmda 7089 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π½) β ((π½ mVar ((πΌ β π½) mPoly π
))βπ) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
210 | 209 | adantlr 713 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β π½) β ((π½ mVar ((πΌ β π½) mPoly π
))βπ) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
211 | 78, 17, 207, 208, 210 | mulgnn0cld 19054 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β π½) β ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
212 | 211 | fmpttd 7120 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))):π½βΆ(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
213 | 114, 191,
180 | fmptssfisupp 9417 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (π β π½ β¦ (πβπ)) finSupp 0) |
214 | 213, 116,
208, 210, 117 | fsuppssov1 9407 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))) finSupp
(0gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
215 | 78, 79, 83, 206, 212, 214 | gsumcl 19874 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
216 | | eqid 2725 |
. . . . . . . . . . . . 13
β’ (
Β·π β(π½ mPoly ((πΌ β π½) mPoly π
))) = ( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
))) |
217 | 5, 27, 144, 15, 18, 216 | asclmul1 21823 |
. . . . . . . . . . . 12
β’ (((π½ 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 π
))βπ)))))) |
218 | 204, 205,
215, 217 | syl3anc 1368 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (((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 π
))βπ)))))) |
219 | 155 | oveqd 7433 |
. . . . . . . . . . . . . . 15
β’ (π β ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)) = ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))) |
220 | 219 | mpteq2dv 5245 |
. . . . . . . . . . . . . 14
β’ (π β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ)))) |
221 | 154, 220 | oveq12d 7434 |
. . . . . . . . . . . . 13
β’ (π β ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)))) = ((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))))) |
222 | 221 | adantr 479 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)))) = ((mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))))(((πΌ β π½) mVar π
)βπ))))) |
223 | 222 | oveq1d 7431 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ 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 π
))βπ)))))) |
224 | 218, 223 | eqtr4d 2768 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (((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β((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))))) |
225 | 125, 203,
224 | 3eqtrd 2769 |
. . . . . . . . 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 π
))βπ)))))) |
226 | 77, 225 | oveq12d 7434 |
. . . . . . . 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 π
))βπ))))))) |
227 | 74, 75 | ffvelcdmd 7090 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)) β (Baseβ((πΌ β π½) mPoly π
))) |
228 | 141 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (Baseβ((πΌ β π½) mPoly π
)) = (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
229 | 227, 228 | eleqtrd 2827 |
. . . . . . . . 9
β’ ((π β§ π β π·) β ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)) β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
230 | 4, 21, 49 | mpllmodd 41833 |
. . . . . . . . . . 11
β’ (π β (π½ mPoly ((πΌ β π½) mPoly π
)) β LMod) |
231 | 230 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (π½ mPoly ((πΌ β π½) mPoly π
)) β LMod) |
232 | | eqid 2725 |
. . . . . . . . . . . 12
β’
(0gβ(mulGrpβ((πΌ β π½) mPoly π
))) =
(0gβ(mulGrpβ((πΌ β π½) mPoly π
))) |
233 | 162 | adantr 479 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (mulGrpβ((πΌ β π½) mPoly π
)) β CMnd) |
234 | 165 | fmpttd 7120 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))):(πΌ β π½)βΆ(Baseβ((πΌ β π½) mPoly π
))) |
235 | 159, 232,
160 | mulg0 19034 |
. . . . . . . . . . . . . 14
β’ (π β (Baseβ((πΌ β π½) mPoly π
)) β
(0(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))π) =
(0gβ(mulGrpβ((πΌ β π½) mPoly π
)))) |
236 | 235 | adantl 480 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π β (Baseβ((πΌ β π½) mPoly π
))) β
(0(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))π) =
(0gβ(mulGrpβ((πΌ β π½) mPoly π
)))) |
237 | | fvexd 6907 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β
(0gβ(mulGrpβ((πΌ β π½) mPoly π
))) β V) |
238 | 181, 236,
139, 140, 237 | fsuppssov1 9407 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))) finSupp
(0gβ(mulGrpβ((πΌ β π½) mPoly π
)))) |
239 | 159, 232,
233, 176, 234, 238 | gsumcl 19874 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)))) β (Baseβ((πΌ β π½) mPoly π
))) |
240 | 239, 228 | eleqtrd 2827 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)))) β (Baseβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
241 | 15, 27, 216, 144, 231, 240, 215 | lmodvscld 20766 |
. . . . . . . . 9
β’ ((π β§ π β π·) β (((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
242 | 5, 27, 144, 15, 18, 216 | asclmul1 21823 |
. . . . . . . . 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 π
))βπ))))))) |
243 | 204, 229,
241, 242 | syl3anc 1368 |
. . . . . . . 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 π
))βπ))))))) |
244 | 226, 243 | eqtrd 2765 |
. . . . . . 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 π
))βπ))))))) |
245 | 244 | mpteq2dva 5243 |
. . . . . 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 π
))βπ)))))))) |
246 | 245 | oveq2d 7432 |
. . . . 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 π
))βπ))))))))) |
247 | 10, 67, 246 | 3eqtrd 2769 |
. . . 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 π
))βπ))))))))) |
248 | 247 | fveq1d 6894 |
. . 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 π
))βπ))))))))β(π βΎ π½))) |
249 | 248 | fveq1d 6894 |
. 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 π
))βπ))))))))β(π βΎ π½))β(π βΎ (πΌ β π½)))) |
250 | | eqid 2725 |
. . . 4
β’
(0gβ((πΌ β π½) mPoly π
)) = (0gβ((πΌ β π½) mPoly π
)) |
251 | 49 | ringcmnd 20224 |
. . . 4
β’ (π β ((πΌ β π½) mPoly π
) β CMnd) |
252 | 7 | crnggrpd 20191 |
. . . . 5
β’ (π β π
β Grp) |
253 | 252 | grpmndd 18907 |
. . . 4
β’ (π β π
β Mnd) |
254 | | ovex 7449 |
. . . . . 6
β’
(β0 βm πΌ) β V |
255 | 14, 254 | rabex2 5331 |
. . . . 5
β’ π· β V |
256 | 255 | a1i 11 |
. . . 4
β’ (π β π· β V) |
257 | | eqid 2725 |
. . . . . 6
β’ {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} = {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β
Fin} |
258 | | eqid 2725 |
. . . . . 6
β’ (π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) = (π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) |
259 | | difssd 4125 |
. . . . . . 7
β’ (π β (πΌ β π½) β πΌ) |
260 | | selvvvval.y |
. . . . . . 7
β’ (π β π β π·) |
261 | 14, 257, 20, 259, 260 | psrbagres 41832 |
. . . . . 6
β’ (π β (π βΎ (πΌ β π½)) β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β
Fin}) |
262 | 3, 54, 257, 258, 22, 252, 261 | mplmapghm 41854 |
. . . . 5
β’ (π β (π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) β (((πΌ β π½) mPoly π
) GrpHom π
)) |
263 | | ghmmhm 19184 |
. . . . 5
β’ ((π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) β (((πΌ β π½) mPoly π
) GrpHom π
) β (π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) β (((πΌ β π½) mPoly π
) MndHom π
)) |
264 | 262, 263 | syl 17 |
. . . 4
β’ (π β (π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) β (((πΌ β π½) mPoly π
) MndHom π
)) |
265 | | eqid 2725 |
. . . . . . . 8
β’ {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β Fin} = {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β
Fin} |
266 | | simpr 483 |
. . . . . . . 8
β’ ((π β§ π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
267 | 4, 54, 15, 265, 266 | mplelf 21947 |
. . . . . . 7
β’ ((π β§ π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β π€:{π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β
Fin}βΆ(Baseβ((πΌ
β π½) mPoly π
))) |
268 | 14, 265, 20, 8, 260 | psrbagres 41832 |
. . . . . . . 8
β’ (π β (π βΎ π½) β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β
Fin}) |
269 | 268 | adantr 479 |
. . . . . . 7
β’ ((π β§ π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β (π βΎ π½) β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β
Fin}) |
270 | 267, 269 | ffvelcdmd 7090 |
. . . . . 6
β’ ((π β§ π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β (π€β(π βΎ π½)) β (Baseβ((πΌ β π½) mPoly π
))) |
271 | 270 | fmpttd 7120 |
. . . . 5
β’ (π β (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))):(Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))βΆ(Baseβ((πΌ β π½) mPoly π
))) |
272 | 15, 27, 216, 144, 231, 229, 241 | lmodvscld 20766 |
. . . . . 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 π
)))) |
273 | 272 | fmpttd 7120 |
. . . . 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 π
)))) |
274 | 271, 273 | fcod 6744 |
. . . 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 π
))) |
275 | | fvexd 6907 |
. . . . 5
β’ (π β
(0gβ((πΌ
β π½) mPoly π
)) β V) |
276 | 24 | crngringd 20190 |
. . . . . 6
β’ (π β (π½ mPoly ((πΌ β π½) mPoly π
)) β Ring) |
277 | | eqid 2725 |
. . . . . . 7
β’
(0gβ(π½ mPoly ((πΌ β π½) mPoly π
))) = (0gβ(π½ mPoly ((πΌ β π½) mPoly π
))) |
278 | 15, 277 | ring0cl 20207 |
. . . . . 6
β’ ((π½ mPoly ((πΌ β π½) mPoly π
)) β Ring β
(0gβ(π½
mPoly ((πΌ β π½) mPoly π
))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
279 | 276, 278 | syl 17 |
. . . . 5
β’ (π β
(0gβ(π½
mPoly ((πΌ β π½) mPoly π
))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
280 | | ssidd 3996 |
. . . . 5
β’ (π β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
281 | 255 | mptex 7231 |
. . . . . . . 8
β’ (π β π· β¦ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))) β V |
282 | 281 | a1i 11 |
. . . . . . 7
β’ (π β (π β π· β¦ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))) β V) |
283 | | fvexd 6907 |
. . . . . . 7
β’ (π β
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β V) |
284 | | funmpt 6586 |
. . . . . . . 8
β’ Fun
(π β π· β¦ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))) |
285 | 284 | a1i 11 |
. . . . . . 7
β’ (π β Fun (π β π· β¦ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)))) |
286 | | eqid 2725 |
. . . . . . . 8
β’
(0gβπ
) = (0gβπ
) |
287 | 1, 2, 286, 9, 7 | mplelsfi 21944 |
. . . . . . 7
β’ (π β πΉ finSupp (0gβπ
)) |
288 | | ssidd 3996 |
. . . . . . . . . . 11
β’ (π β (πΉ supp (0gβπ
)) β (πΉ supp (0gβπ
))) |
289 | | fvexd 6907 |
. . . . . . . . . . 11
β’ (π β (0gβπ
) β V) |
290 | 69, 288, 9, 289 | suppssrg 8200 |
. . . . . . . . . 10
β’ ((π β§ π β (π· β (πΉ supp (0gβπ
)))) β (πΉβπ) = (0gβπ
)) |
291 | 290 | fveq2d 6896 |
. . . . . . . . 9
β’ ((π β§ π β (π· β (πΉ supp (0gβπ
)))) β ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)) = ((algScβ((πΌ β π½) mPoly π
))β(0gβπ
))) |
292 | 3, 32, 286, 250, 22, 58 | mplascl0 41852 |
. . . . . . . . . . 11
β’ (π β ((algScβ((πΌ β π½) mPoly π
))β(0gβπ
)) =
(0gβ((πΌ
β π½) mPoly π
))) |
293 | 38 | fveq2d 6896 |
. . . . . . . . . . 11
β’ (π β
(0gβ((πΌ
β π½) mPoly π
)) =
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
294 | 292, 293 | eqtrd 2765 |
. . . . . . . . . 10
β’ (π β ((algScβ((πΌ β π½) mPoly π
))β(0gβπ
)) =
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
295 | 294 | adantr 479 |
. . . . . . . . 9
β’ ((π β§ π β (π· β (πΉ supp (0gβπ
)))) β ((algScβ((πΌ β π½) mPoly π
))β(0gβπ
)) =
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
296 | 291, 295 | eqtrd 2765 |
. . . . . . . 8
β’ ((π β§ π β (π· β (πΉ supp (0gβπ
)))) β ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ)) =
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
297 | 296, 256 | suppss2 8204 |
. . . . . . 7
β’ (π β ((π β π· β¦ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))) supp
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) β (πΉ supp (0gβπ
))) |
298 | 282, 283,
285, 287, 297 | fsuppsssuppgd 9405 |
. . . . . 6
β’ (π β (π β π· β¦ ((algScβ((πΌ β π½) mPoly π
))β(πΉβπ))) finSupp
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))) |
299 | | eqid 2725 |
. . . . . . . 8
β’
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) =
(0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
300 | 15, 27, 216, 299, 277 | lmod0vs 20782 |
. . . . . . 7
β’ (((π½ mPoly ((πΌ β π½) mPoly π
)) β LMod β§ π β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β
((0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))π) = (0gβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
301 | 230, 300 | sylan 578 |
. . . . . 6
β’ ((π β§ π β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
)))) β
((0gβ(Scalarβ(π½ mPoly ((πΌ β π½) mPoly π
))))( Β·π
β(π½ mPoly ((πΌ β π½) mPoly π
)))π) = (0gβ(π½ mPoly ((πΌ β π½) mPoly π
)))) |
302 | | fvexd 6907 |
. . . . . 6
β’ (π β
(0gβ(π½
mPoly ((πΌ β π½) mPoly π
))) β V) |
303 | 298, 301,
227, 241, 302 | fsuppssov1 9407 |
. . . . 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 π
)))) |
304 | | eqid 2725 |
. . . . . . . 8
β’ (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) = (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) |
305 | 23 | crnggrpd 20191 |
. . . . . . . 8
β’ (π β ((πΌ β π½) mPoly π
) β Grp) |
306 | 4, 15, 265, 304, 21, 305, 268 | mplmapghm 41854 |
. . . . . . 7
β’ (π β (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β ((π½ mPoly ((πΌ β π½) mPoly π
)) GrpHom ((πΌ β π½) mPoly π
))) |
307 | | ghmmhm 19184 |
. . . . . . 7
β’ ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β ((π½ mPoly ((πΌ β π½) mPoly π
)) GrpHom ((πΌ β π½) mPoly π
)) β (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β ((π½ mPoly ((πΌ β π½) mPoly π
)) MndHom ((πΌ β π½) mPoly π
))) |
308 | 306, 307 | syl 17 |
. . . . . 6
β’ (π β (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β ((π½ mPoly ((πΌ β π½) mPoly π
)) MndHom ((πΌ β π½) mPoly π
))) |
309 | 277, 250 | mhm0 18750 |
. . . . . 6
β’ ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) β ((π½ mPoly ((πΌ β π½) mPoly π
)) MndHom ((πΌ β π½) mPoly π
)) β ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½)))β(0gβ(π½ mPoly ((πΌ β π½) mPoly π
)))) = (0gβ((πΌ β π½) mPoly π
))) |
310 | 308, 309 | syl 17 |
. . . . 5
β’ (π β ((π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½)))β(0gβ(π½ mPoly ((πΌ β π½) mPoly π
)))) = (0gβ((πΌ β π½) mPoly π
))) |
311 | 275, 279,
273, 271, 280, 256, 47, 303, 310 | fsuppcor 9427 |
. . . 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 π
))) |
312 | 54, 250, 251, 253, 256, 264, 274, 311 | gsummhm 19897 |
. . 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 π
))βπ))))))))))) |
313 | | fveq1 6891 |
. . . 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 π
))βπ)))))))))β(π βΎ (πΌ β π½)))) |
314 | 54, 250, 251, 256, 274, 311 | gsumcl 19874 |
. . . 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 π
))) |
315 | | fvexd 6907 |
. . . 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) |
316 | 258, 313,
314, 315 | fvmptd3 7023 |
. . 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 π
))βπ)))))))))β(π βΎ (πΌ β π½)))) |
317 | 276 | ringcmnd 20224 |
. . . . . 6
β’ (π β (π½ mPoly ((πΌ β π½) mPoly π
)) β CMnd) |
318 | 305 | grpmndd 18907 |
. . . . . 6
β’ (π β ((πΌ β π½) mPoly π
) β Mnd) |
319 | 15, 277, 317, 318, 256, 308, 273, 303 | gsummhm 19897 |
. . . . 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 π
))βπ)))))))))) |
320 | | fveq1 6891 |
. . . . . 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 π
))βπ))))))))β(π βΎ π½))) |
321 | 15, 277, 317, 256, 273, 303 | gsumcl 19874 |
. . . . . 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 π
)))) |
322 | | fvexd 6907 |
. . . . . 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) |
323 | 304, 320,
321, 322 | fvmptd3 7023 |
. . . . 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 π
))βπ))))))))β(π βΎ π½))) |
324 | 319, 323 | eqtrd 2765 |
. . . 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 π
))βπ))))))))β(π βΎ π½))) |
325 | 324 | fveq1d 6894 |
. . 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 π
))βπ))))))))β(π βΎ π½))β(π βΎ (πΌ β π½)))) |
326 | 312, 316,
325 | 3eqtrrd 2770 |
. 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 π
))βπ))))))))))) |
327 | 4, 54, 15, 265, 272 | mplelf 21947 |
. . . . . . 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 π
))) |
328 | 268 | adantr 479 |
. . . . . . 7
β’ ((π β§ π β π·) β (π βΎ π½) β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β
Fin}) |
329 | 327, 328 | ffvelcdmd 7090 |
. . . . . 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 π
))) |
330 | | eqidd 2726 |
. . . . . . 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 π
))βπ)))))))) |
331 | | eqidd 2726 |
. . . . . . 7
β’ (π β (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½))) = (π€ β (Baseβ(π½ mPoly ((πΌ β π½) mPoly π
))) β¦ (π€β(π βΎ π½)))) |
332 | | fveq1 6891 |
. . . . . . 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 π
))βπ))))))β(π βΎ π½))) |
333 | 272, 330,
331, 332 | fmptco 7134 |
. . . . . 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 π
))βπ))))))β(π βΎ π½)))) |
334 | | eqidd 2726 |
. . . . . 6
β’ (π β (π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½)))) = (π£ β (Baseβ((πΌ β π½) mPoly π
)) β¦ (π£β(π βΎ (πΌ β π½))))) |
335 | | fveq1 6891 |
. . . . . 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 π
))βπ))))))β(π βΎ π½))β(π βΎ (πΌ β π½)))) |
336 | 329, 333,
334, 335 | fmptco 7134 |
. . . . 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 π
))βπ))))))β(π βΎ π½))β(π βΎ (πΌ β π½))))) |
337 | | eqid 2725 |
. . . . . . . . . 10
β’
(.rβ((πΌ β π½) mPoly π
)) = (.rβ((πΌ β π½) mPoly π
)) |
338 | 4, 216, 54, 15, 337, 265, 227, 241, 328 | mplvscaval 21965 |
. . . . . . . . 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 π
))βπ)))))β(π βΎ π½)))) |
339 | 4, 216, 54, 15, 337, 265, 239, 215, 328 | mplvscaval 21965 |
. . . . . . . . . 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 π
))βπ))))β(π βΎ π½)))) |
340 | 339 | oveq2d 7432 |
. . . . . . . . 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 π
))βπ))))β(π βΎ π½))))) |
341 | 31 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β ((πΌ β π½) mPoly π
) β AssAlg) |
342 | 36 | fveq2d 6896 |
. . . . . . . . . . . 12
β’ (π β (Baseβπ
) =
(Baseβ(Scalarβ((πΌ β π½) mPoly π
)))) |
343 | 342 | adantr 479 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (Baseβπ
) = (Baseβ(Scalarβ((πΌ β π½) mPoly π
)))) |
344 | 75, 343 | eleqtrd 2827 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (πΉβπ) β (Baseβ(Scalarβ((πΌ β π½) mPoly π
)))) |
345 | 49 | adantr 479 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β ((πΌ β π½) mPoly π
) β Ring) |
346 | 4, 54, 15, 265, 215 | mplelf 21947 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))):{π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β
Fin}βΆ(Baseβ((πΌ
β π½) mPoly π
))) |
347 | 346, 328 | ffvelcdmd 7090 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½)) β (Baseβ((πΌ β π½) mPoly π
))) |
348 | 54, 337, 345, 239, 347 | ringcld 20203 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½))) β (Baseβ((πΌ β π½) mPoly π
))) |
349 | | eqid 2725 |
. . . . . . . . . . 11
β’
(Baseβ(Scalarβ((πΌ β π½) mPoly π
))) = (Baseβ(Scalarβ((πΌ β π½) mPoly π
))) |
350 | | eqid 2725 |
. . . . . . . . . . 11
β’ (
Β·π β((πΌ β π½) mPoly π
)) = ( Β·π
β((πΌ β π½) mPoly π
)) |
351 | 32, 33, 349, 54, 337, 350 | asclmul1 21823 |
. . . . . . . . . 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 π
))βπ))))β(π βΎ π½))))) |
352 | 341, 344,
348, 351 | syl3anc 1368 |
. . . . . . . . 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 π
))βπ))))β(π βΎ π½))))) |
353 | 338, 340,
352 | 3eqtrd 2769 |
. . . . . . . 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 π
))βπ))))β(π βΎ π½))))) |
354 | 353 | fveq1d 6894 |
. . . . . . 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 π
))βπ))))β(π βΎ π½))))β(π βΎ (πΌ β π½)))) |
355 | | eqid 2725 |
. . . . . . . 8
β’
(.rβπ
) = (.rβπ
) |
356 | 261 | adantr 479 |
. . . . . . . 8
β’ ((π β§ π β π·) β (π βΎ (πΌ β π½)) β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β
Fin}) |
357 | 3, 350, 68, 54, 355, 257, 75, 348, 356 | mplvscaval 21965 |
. . . . . . 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 π
))βπ))))β(π βΎ π½)))β(π βΎ (πΌ β π½))))) |
358 | | ovif2 7516 |
. . . . . . . . . . . . 13
β’ ((π β {π¦ β (β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 π
)))) |
359 | 358 | fveq1i 6893 |
. . . . . . . . . . . 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 π
))))β(π βΎ (πΌ β π½))) |
360 | | iffv 6909 |
. . . . . . . . . . . 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 π
)))β(π βΎ (πΌ β π½)))) |
361 | 359, 360 | eqtri 2753 |
. . . . . . . . . . 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 π
)))β(π βΎ (πΌ β π½)))) |
362 | | eqeq1 2729 |
. . . . . . . . . . . . . 14
β’ (π = (π βΎ (πΌ β π½)) β (π = (π βΎ (πΌ β π½)) β (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)))) |
363 | 362 | ifbid 4547 |
. . . . . . . . . . . . 13
β’ (π = (π βΎ (πΌ β π½)) β if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)) = if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
))) |
364 | | eqid 2725 |
. . . . . . . . . . . . . 14
β’
(1rβ((πΌ β π½) mPoly π
)) = (1rβ((πΌ β π½) mPoly π
)) |
365 | | eqid 2725 |
. . . . . . . . . . . . . . 15
β’
(1rβπ
) = (1rβπ
) |
366 | 58 | adantr 479 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β π
β Ring) |
367 | 14, 257, 84, 151, 71 | psrbagres 41832 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (π βΎ (πΌ β π½)) β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β
Fin}) |
368 | 3, 54, 286, 365, 257, 176, 366, 367 | mplmon 21980 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
))) β (Baseβ((πΌ β π½) mPoly π
))) |
369 | 54, 337, 364, 345, 368 | ringridmd 20213 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(1rβ((πΌ β π½) mPoly π
))) = (π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))) |
370 | | fvexd 6907 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (1rβπ
) β V) |
371 | | fvexd 6907 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (0gβπ
) β V) |
372 | 370, 371 | ifcld 4570 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)) β V) |
373 | 363, 369,
356, 372 | fvmptd4 7024 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(1rβ((πΌ β π½) mPoly π
)))β(π βΎ (πΌ β π½))) = if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
))) |
374 | 54, 337, 250, 345, 368 | ringrzd 20236 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(0gβ((πΌ β π½) mPoly π
))) = (0gβ((πΌ β π½) mPoly π
))) |
375 | 3, 257, 286, 250, 22, 252 | mpl0 21955 |
. . . . . . . . . . . . . . . 16
β’ (π β
(0gβ((πΌ
β π½) mPoly π
)) = ({π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} Γ
{(0gβπ
)})) |
376 | 375 | adantr 479 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (0gβ((πΌ β π½) mPoly π
)) = ({π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} Γ
{(0gβπ
)})) |
377 | 374, 376 | eqtrd 2765 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β ((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(0gβ((πΌ β π½) mPoly π
))) = ({π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} Γ
{(0gβπ
)})) |
378 | 377 | fveq1d 6894 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(0gβ((πΌ β π½) mPoly π
)))β(π βΎ (πΌ β π½))) = (({π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} Γ
{(0gβπ
)})β(π βΎ (πΌ β π½)))) |
379 | | fvex 6905 |
. . . . . . . . . . . . . . 15
β’
(0gβπ
) β V |
380 | 379 | fvconst2 7212 |
. . . . . . . . . . . . . 14
β’ ((π βΎ (πΌ β π½)) β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β (({π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} Γ
{(0gβπ
)})β(π βΎ (πΌ β π½))) = (0gβπ
)) |
381 | 356, 380 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (({π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} Γ
{(0gβπ
)})β(π βΎ (πΌ β π½))) = (0gβπ
)) |
382 | 378, 381 | eqtrd 2765 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))(0gβ((πΌ β π½) mPoly π
)))β(π βΎ (πΌ β π½))) = (0gβπ
)) |
383 | 373, 382 | ifeq12d 4545 |
. . . . . . . . . . 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βπ
))) |
384 | 361, 383 | eqtrid 2777 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))))β(π βΎ (πΌ β π½))) = if((π βΎ π½) = (π βΎ π½), if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)), (0gβπ
))) |
385 | 384 | oveq2d 7432 |
. . . . . . . . 9
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)(((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))))β(π βΎ (πΌ β π½)))) = ((πΉβπ)(.rβπ
)if((π βΎ π½) = (π βΎ π½), if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)), (0gβπ
)))) |
386 | | ifan 4577 |
. . . . . . . . . . 11
β’
if(((π βΎ π½) = (π βΎ π½) β§ (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½))), (1rβπ
), (0gβπ
)) = if((π βΎ π½) = (π βΎ π½), if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)), (0gβπ
)) |
387 | 386 | oveq2i 7427 |
. . . . . . . . . 10
β’ ((πΉβπ)(.rβπ
)if(((π βΎ π½) = (π βΎ π½) β§ (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½))), (1rβπ
), (0gβπ
))) = ((πΉβπ)(.rβπ
)if((π βΎ π½) = (π βΎ π½), if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)), (0gβπ
))) |
388 | 14 | psrbagf 21855 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π· β π:πΌβΆβ0) |
389 | 260, 388 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β π:πΌβΆβ0) |
390 | 389 | ffnd 6718 |
. . . . . . . . . . . . . . . 16
β’ (π β π Fn πΌ) |
391 | 390 | adantr 479 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β π Fn πΌ) |
392 | | undif 4477 |
. . . . . . . . . . . . . . . . . 18
β’ (π½ β πΌ β (π½ βͺ (πΌ β π½)) = πΌ) |
393 | 8, 392 | sylib 217 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π½ βͺ (πΌ β π½)) = πΌ) |
394 | 393 | adantr 479 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β (π½ βͺ (πΌ β π½)) = πΌ) |
395 | 394 | fneq2d 6643 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (π Fn (π½ βͺ (πΌ β π½)) β π Fn πΌ)) |
396 | 391, 395 | mpbird 256 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β π Fn (π½ βͺ (πΌ β π½))) |
397 | 88 | ffnd 6718 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β π Fn πΌ) |
398 | 394 | fneq2d 6643 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (π Fn (π½ βͺ (πΌ β π½)) β π Fn πΌ)) |
399 | 397, 398 | mpbird 256 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β π Fn (π½ βͺ (πΌ β π½))) |
400 | | eqfnun 7041 |
. . . . . . . . . . . . . 14
β’ ((π Fn (π½ βͺ (πΌ β π½)) β§ π Fn (π½ βͺ (πΌ β π½))) β (π = π β ((π βΎ π½) = (π βΎ π½) β§ (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½))))) |
401 | 396, 399,
400 | syl2anc 582 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (π = π β ((π βΎ π½) = (π βΎ π½) β§ (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½))))) |
402 | 401 | ifbid 4547 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β if(π = π, (1rβπ
), (0gβπ
)) = if(((π βΎ π½) = (π βΎ π½) β§ (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½))), (1rβπ
), (0gβπ
))) |
403 | 402 | oveq2d 7432 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)if(π = π, (1rβπ
), (0gβπ
))) = ((πΉβπ)(.rβπ
)if(((π βΎ π½) = (π βΎ π½) β§ (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½))), (1rβπ
), (0gβπ
)))) |
404 | | ovif2 7516 |
. . . . . . . . . . 11
β’ ((πΉβπ)(.rβπ
)if(π = π, (1rβπ
), (0gβπ
))) = if(π = π, ((πΉβπ)(.rβπ
)(1rβπ
)), ((πΉβπ)(.rβπ
)(0gβπ
))) |
405 | 403, 404 | eqtr3di 2780 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)if(((π βΎ π½) = (π βΎ π½) β§ (π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½))), (1rβπ
), (0gβπ
))) = if(π = π, ((πΉβπ)(.rβπ
)(1rβπ
)), ((πΉβπ)(.rβπ
)(0gβπ
)))) |
406 | 387, 405 | eqtr3id 2779 |
. . . . . . . . 9
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)if((π βΎ π½) = (π βΎ π½), if((π βΎ (πΌ β π½)) = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)), (0gβπ
))) = if(π = π, ((πΉβπ)(.rβπ
)(1rβπ
)), ((πΉβπ)(.rβπ
)(0gβπ
)))) |
407 | 385, 406 | eqtrd 2765 |
. . . . . . . 8
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)(((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))))β(π βΎ (πΌ β π½)))) = if(π = π, ((πΉβπ)(.rβπ
)(1rβπ
)), ((πΉβπ)(.rβπ
)(0gβπ
)))) |
408 | 7 | adantr 479 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β π
β CRing) |
409 | 3, 257, 286, 365, 176, 158, 160, 57, 408, 367 | mplcoe2 21986 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
))) = ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))) |
410 | | simpr 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β π β (πΌ β π½)) |
411 | 410 | fvresd 6912 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β ((π βΎ (πΌ β π½))βπ) = (πβπ)) |
412 | 411 | oveq1d 7431 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β (πΌ β π½)) β (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)) = ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))) |
413 | 412 | mpteq2dva 5243 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)))) |
414 | 413 | oveq2d 7432 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ)))) = ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))) |
415 | 409, 414 | eqtrd 2765 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
))) = ((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))) |
416 | | eqid 2725 |
. . . . . . . . . . . . 13
β’ (π β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β Fin} β¦
if(π = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
)))) = (π β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β Fin} β¦
if(π = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
)))) |
417 | | eqeq1 2729 |
. . . . . . . . . . . . . 14
β’ (π = (π βΎ π½) β (π = (π βΎ π½) β (π βΎ π½) = (π βΎ π½))) |
418 | 417 | ifbid 4547 |
. . . . . . . . . . . . 13
β’ (π = (π βΎ π½) β if(π = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))) = if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
)))) |
419 | | fvexd 6907 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (1rβ((πΌ β π½) mPoly π
)) β V) |
420 | | fvexd 6907 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (0gβ((πΌ β π½) mPoly π
)) β V) |
421 | 419, 420 | ifcld 4570 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))) β V) |
422 | 416, 418,
328, 421 | fvmptd3 7023 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β ((π β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β Fin} β¦
if(π = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))))β(π βΎ π½)) = if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
)))) |
423 | 23 | adantr 479 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β ((πΌ β π½) mPoly π
) β CRing) |
424 | 14, 265, 84, 191, 71 | psrbagres 41832 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (π βΎ π½) β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β
Fin}) |
425 | 4, 265, 250, 364, 206, 16, 17, 48, 423, 424 | mplcoe2 21986 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (π β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β Fin} β¦
if(π = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
)))) = ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))) |
426 | | simpr 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β π½) β π β π½) |
427 | 426 | fvresd 6912 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β π½) β ((π βΎ π½)βπ) = (πβπ)) |
428 | 427 | oveq1d 7431 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β π½) β (((π βΎ π½)βπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)) = ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))) |
429 | 428 | mpteq2dva 5243 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))) |
430 | 429 | oveq2d 7432 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ)))) = ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))) |
431 | 425, 430 | eqtrd 2765 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β (π β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β Fin} β¦
if(π = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
)))) = ((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))) |
432 | 431 | fveq1d 6894 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β ((π β {π₯ β (β0
βm π½)
β£ (β‘π₯ β β) β Fin} β¦
if(π = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))))β(π βΎ π½)) = (((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½))) |
433 | 422, 432 | eqtr3d 2767 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))) = (((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½))) |
434 | 415, 433 | oveq12d 7434 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β ((π β {π¦ β (β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 π
))βπ))))β(π βΎ π½)))) |
435 | 434 | fveq1d 6894 |
. . . . . . . . 9
β’ ((π β§ π β π·) β (((π β {π¦ β (β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 π
))βπ))))β(π βΎ π½)))β(π βΎ (πΌ β π½)))) |
436 | 435 | oveq2d 7432 |
. . . . . . . 8
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)(((π β {π¦ β (β0
βm (πΌ
β π½)) β£ (β‘π¦ β β) β Fin} β¦
if(π = (π βΎ (πΌ β π½)), (1rβπ
), (0gβπ
)))(.rβ((πΌ β π½) mPoly π
))if((π βΎ π½) = (π βΎ π½), (1rβ((πΌ β π½) mPoly π
)), (0gβ((πΌ β π½) mPoly π
))))β(π βΎ (πΌ β π½)))) = ((πΉβπ)(.rβπ
)((((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½)))β(π βΎ (πΌ β π½))))) |
437 | 68, 355, 365, 366, 75 | ringridmd 20213 |
. . . . . . . . 9
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)(1rβπ
)) = (πΉβπ)) |
438 | 68, 355, 286, 366, 75 | ringrzd 20236 |
. . . . . . . . 9
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)(0gβπ
)) = (0gβπ
)) |
439 | 437, 438 | ifeq12d 4545 |
. . . . . . . 8
β’ ((π β§ π β π·) β if(π = π, ((πΉβπ)(.rβπ
)(1rβπ
)), ((πΉβπ)(.rβπ
)(0gβπ
))) = if(π = π, (πΉβπ), (0gβπ
))) |
440 | 407, 436,
439 | 3eqtr3d 2773 |
. . . . . . 7
β’ ((π β§ π β π·) β ((πΉβπ)(.rβπ
)((((mulGrpβ((πΌ β π½) mPoly π
)) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβ((πΌ β π½) mPoly π
)))(((πΌ β π½) mVar π
)βπ))))(.rβ((πΌ β π½) mPoly π
))(((mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβ(π½ mPoly ((πΌ β π½) mPoly π
))))((π½ mVar ((πΌ β π½) mPoly π
))βπ))))β(π βΎ π½)))β(π βΎ (πΌ β π½)))) = if(π = π, (πΉβπ), (0gβπ
))) |
441 | 354, 357,
440 | 3eqtrd 2769 |
. . . . . 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βπ
))) |
442 | 441 | mpteq2dva 5243 |
. . . . 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βπ
)))) |
443 | 336, 442 | eqtrd 2765 |
. . . 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βπ
)))) |
444 | 443 | oveq2d 7432 |
. . 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βπ
))))) |
445 | 58 | ringcmnd 20224 |
. . . 4
β’ (π β π
β CMnd) |
446 | 68, 286 | ring0cl 20207 |
. . . . . . . 8
β’ (π
β Ring β
(0gβπ
)
β (Baseβπ
)) |
447 | 58, 446 | syl 17 |
. . . . . . 7
β’ (π β (0gβπ
) β (Baseβπ
)) |
448 | 447 | adantr 479 |
. . . . . 6
β’ ((π β§ π β π·) β (0gβπ
) β (Baseβπ
)) |
449 | 75, 448 | ifcld 4570 |
. . . . 5
β’ ((π β§ π β π·) β if(π = π, (πΉβπ), (0gβπ
)) β (Baseβπ
)) |
450 | 449 | fmpttd 7120 |
. . . 4
β’ (π β (π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))):π·βΆ(Baseβπ
)) |
451 | | eldifsnneq 4790 |
. . . . . . . 8
β’ (π β (π· β {π}) β Β¬ π = π) |
452 | 451 | neqcomd 2735 |
. . . . . . 7
β’ (π β (π· β {π}) β Β¬ π = π) |
453 | 452 | iffalsed 4535 |
. . . . . 6
β’ (π β (π· β {π}) β if(π = π, (πΉβπ), (0gβπ
)) = (0gβπ
)) |
454 | 453 | adantl 480 |
. . . . 5
β’ ((π β§ π β (π· β {π})) β if(π = π, (πΉβπ), (0gβπ
)) = (0gβπ
)) |
455 | 454, 256 | suppss2 8204 |
. . . 4
β’ (π β ((π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) supp (0gβπ
)) β {π}) |
456 | 256 | mptexd 7232 |
. . . . 5
β’ (π β (π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) β V) |
457 | | funmpt 6586 |
. . . . . 6
β’ Fun
(π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) |
458 | 457 | a1i 11 |
. . . . 5
β’ (π β Fun (π β π· β¦ if(π = π, (πΉβπ), (0gβπ
)))) |
459 | | snfi 9067 |
. . . . . . 7
β’ {π} β Fin |
460 | 459 | a1i 11 |
. . . . . 6
β’ (π β {π} β Fin) |
461 | 460, 455 | ssfid 9290 |
. . . . 5
β’ (π β ((π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) supp (0gβπ
)) β Fin) |
462 | 456, 447,
458, 461 | isfsuppd 9390 |
. . . 4
β’ (π β (π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) finSupp (0gβπ
)) |
463 | 68, 286, 445, 256, 450, 455, 462 | gsumres 19872 |
. . 3
β’ (π β (π
Ξ£g ((π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) βΎ {π})) = (π
Ξ£g (π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))))) |
464 | 260 | snssd 4808 |
. . . . . 6
β’ (π β {π} β π·) |
465 | 464 | resmptd 6039 |
. . . . 5
β’ (π β ((π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) βΎ {π}) = (π β {π} β¦ if(π = π, (πΉβπ), (0gβπ
)))) |
466 | 465 | oveq2d 7432 |
. . . 4
β’ (π β (π
Ξ£g ((π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) βΎ {π})) = (π
Ξ£g (π β {π} β¦ if(π = π, (πΉβπ), (0gβπ
))))) |
467 | 69, 260 | ffvelcdmd 7090 |
. . . . 5
β’ (π β (πΉβπ) β (Baseβπ
)) |
468 | | iftrue 4530 |
. . . . . . . 8
β’ (π = π β if(π = π, (πΉβπ), (0gβπ
)) = (πΉβπ)) |
469 | 468 | eqcoms 2733 |
. . . . . . 7
β’ (π = π β if(π = π, (πΉβπ), (0gβπ
)) = (πΉβπ)) |
470 | | fveq2 6892 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
471 | 469, 470 | eqtrd 2765 |
. . . . . 6
β’ (π = π β if(π = π, (πΉβπ), (0gβπ
)) = (πΉβπ)) |
472 | 68, 471 | gsumsn 19913 |
. . . . 5
β’ ((π
β Mnd β§ π β π· β§ (πΉβπ) β (Baseβπ
)) β (π
Ξ£g (π β {π} β¦ if(π = π, (πΉβπ), (0gβπ
)))) = (πΉβπ)) |
473 | 253, 260,
467, 472 | syl3anc 1368 |
. . . 4
β’ (π β (π
Ξ£g (π β {π} β¦ if(π = π, (πΉβπ), (0gβπ
)))) = (πΉβπ)) |
474 | 466, 473 | eqtrd 2765 |
. . 3
β’ (π β (π
Ξ£g ((π β π· β¦ if(π = π, (πΉβπ), (0gβπ
))) βΎ {π})) = (πΉβπ)) |
475 | 444, 463,
474 | 3eqtr2d 2771 |
. 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 π
))βπ)))))))))) = (πΉβπ)) |
476 | 249, 326,
475 | 3eqtrd 2769 |
1
β’ (π β (((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½))) = (πΉβπ)) |