Step | Hyp | Ref
| Expression |
1 | | eqid 2728 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
2 | | eqid 2728 |
. . . . . . . . . . . . 13
β’
(.rβπ) = (.rβπ) |
3 | | evlselv.u |
. . . . . . . . . . . . . . . 16
β’ π = ((πΌ β π½) mPoly π
) |
4 | | evlselv.i |
. . . . . . . . . . . . . . . . 17
β’ (π β πΌ β π) |
5 | | difssd 4133 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΌ β π½) β πΌ) |
6 | 4, 5 | ssexd 5328 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΌ β π½) β V) |
7 | | evlselv.r |
. . . . . . . . . . . . . . . 16
β’ (π β π
β CRing) |
8 | 3, 6, 7 | mplcrngd 41810 |
. . . . . . . . . . . . . . 15
β’ (π β π β CRing) |
9 | 8 | crngringd 20193 |
. . . . . . . . . . . . . 14
β’ (π β π β Ring) |
10 | 9 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π β Ring) |
11 | | evlselv.t |
. . . . . . . . . . . . . . . 16
β’ π = (π½ mPoly π) |
12 | | eqid 2728 |
. . . . . . . . . . . . . . . 16
β’
(Baseβπ) =
(Baseβπ) |
13 | | eqid 2728 |
. . . . . . . . . . . . . . . 16
β’ {π β (β0
βm π½)
β£ (β‘π β β) β Fin} = {π β (β0
βm π½)
β£ (β‘π β β) β
Fin} |
14 | | evlselv.p |
. . . . . . . . . . . . . . . . 17
β’ π = (πΌ mPoly π
) |
15 | | evlselv.b |
. . . . . . . . . . . . . . . . 17
β’ π΅ = (Baseβπ) |
16 | | evlselv.j |
. . . . . . . . . . . . . . . . 17
β’ (π β π½ β πΌ) |
17 | | evlselv.f |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ β π΅) |
18 | 14, 15, 3, 11, 12, 4, 7, 16, 17 | selvcl 41847 |
. . . . . . . . . . . . . . . 16
β’ (π β (((πΌ selectVars π
)βπ½)βπΉ) β (Baseβπ)) |
19 | 11, 1, 12, 13, 18 | mplelf 21947 |
. . . . . . . . . . . . . . 15
β’ (π β (((πΌ selectVars π
)βπ½)βπΉ):{π β (β0
βm π½)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ)) |
20 | 19 | adantr 479 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(((πΌ selectVars π
)βπ½)βπΉ):{π β (β0
βm π½)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ)) |
21 | 20 | ffvelcdmda 7099 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ)βπ) β (Baseβπ)) |
22 | | eqid 2728 |
. . . . . . . . . . . . . 14
β’
(mulGrpβπ) =
(mulGrpβπ) |
23 | | eqid 2728 |
. . . . . . . . . . . . . 14
β’
(.gβ(mulGrpβπ)) =
(.gβ(mulGrpβπ)) |
24 | 4, 16 | ssexd 5328 |
. . . . . . . . . . . . . . 15
β’ (π β π½ β V) |
25 | 24 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π½ β V) |
26 | 8 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π β CRing) |
27 | | fvexd 6917 |
. . . . . . . . . . . . . . . . 17
β’ (π β (Baseβπ) β V) |
28 | | evlselv.k |
. . . . . . . . . . . . . . . . . . 19
β’ πΎ = (Baseβπ
) |
29 | 28 | fvexi 6916 |
. . . . . . . . . . . . . . . . . 18
β’ πΎ β V |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΎ β V) |
31 | | evlselv.l |
. . . . . . . . . . . . . . . . . 18
β’ πΏ = (algScβπ) |
32 | 7 | crngringd 20193 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π
β Ring) |
33 | 3, 1, 28, 31, 6, 32 | mplasclf 22016 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΏ:πΎβΆ(Baseβπ)) |
34 | 27, 30, 33 | elmapdd 8866 |
. . . . . . . . . . . . . . . 16
β’ (π β πΏ β ((Baseβπ) βm πΎ)) |
35 | | evlselv.a |
. . . . . . . . . . . . . . . . 17
β’ (π β π΄ β (πΎ βm πΌ)) |
36 | 35, 16 | elmapssresd 41763 |
. . . . . . . . . . . . . . . 16
β’ (π β (π΄ βΎ π½) β (πΎ βm π½)) |
37 | 34, 36 | mapcod 41764 |
. . . . . . . . . . . . . . 15
β’ (π β (πΏ β (π΄ βΎ π½)) β ((Baseβπ) βm π½)) |
38 | 37 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (πΏ β (π΄ βΎ π½)) β ((Baseβπ) βm π½)) |
39 | | simpr 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π β {π β (β0
βm π½)
β£ (β‘π β β) β
Fin}) |
40 | 13, 1, 22, 23, 25, 26, 38, 39 | evlsvvvallem 41825 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβπ)
Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))) β (Baseβπ)) |
41 | 1, 2, 10, 21, 40 | ringcld 20206 |
. . . . . . . . . . . 12
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))) β (Baseβπ)) |
42 | | eqidd 2729 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))) = (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))) |
43 | | eqidd 2729 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π’ β (Baseβπ) β¦ (π’βπ)) = (π’ β (Baseβπ) β¦ (π’βπ))) |
44 | | fveq1 6901 |
. . . . . . . . . . . 12
β’ (π’ = (((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))) β (π’βπ) = ((((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))βπ)) |
45 | 41, 42, 43, 44 | fmptco 7144 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β ((π’ β (Baseβπ) β¦ (π’βπ)) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))) = (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))βπ))) |
46 | 33 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β πΏ:πΎβΆ(Baseβπ)) |
47 | | eqid 2728 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
48 | 47, 28 | mgpbas 20087 |
. . . . . . . . . . . . . . . . . . . . 21
β’ πΎ =
(Baseβ(mulGrpβπ
)) |
49 | | eqid 2728 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(.gβ(mulGrpβπ
)) =
(.gβ(mulGrpβπ
)) |
50 | 47 | ringmgp 20186 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π
β Ring β
(mulGrpβπ
) β
Mnd) |
51 | 32, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (mulGrpβπ
) β Mnd) |
52 | 51 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β (mulGrpβπ
) β Mnd) |
53 | 13 | psrbagf 21858 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β π:π½βΆβ0) |
54 | 53 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π:π½βΆβ0) |
55 | 54 | ffvelcdmda 7099 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β (πβπ) β
β0) |
56 | | elmapi 8874 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π΄ β (πΎ βm πΌ) β π΄:πΌβΆπΎ) |
57 | 35, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π΄:πΌβΆπΎ) |
58 | 57, 16 | fssresd 6769 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π΄ βΎ π½):π½βΆπΎ) |
59 | 58 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π΄ βΎ π½):π½βΆπΎ) |
60 | 59 | ffvelcdmda 7099 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β ((π΄ βΎ π½)βπ) β πΎ) |
61 | 48, 49, 52, 55, 60 | mulgnn0cld 19057 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) β πΎ) |
62 | 46, 61 | cofmpt 7147 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (πΏ β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) = (π β π½ β¦ (πΏβ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) |
63 | 3 | mplassa 21971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((πΌ β π½) β V β§ π
β CRing) β π β AssAlg) |
64 | 6, 7, 63 | syl2anc 582 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π β AssAlg) |
65 | | eqid 2728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(Scalarβπ) =
(Scalarβπ) |
66 | 31, 65 | asclrhm 21830 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β AssAlg β πΏ β ((Scalarβπ) RingHom π)) |
67 | 64, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β πΏ β ((Scalarβπ) RingHom π)) |
68 | 3, 6, 7 | mplsca 21962 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π
= (Scalarβπ)) |
69 | 68 | eqcomd 2734 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (Scalarβπ) = π
) |
70 | 69 | oveq1d 7441 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β ((Scalarβπ) RingHom π) = (π
RingHom π)) |
71 | 67, 70 | eleqtrd 2831 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΏ β (π
RingHom π)) |
72 | 47, 22 | rhmmhm 20425 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (πΏ β (π
RingHom π) β πΏ β ((mulGrpβπ
) MndHom (mulGrpβπ))) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β πΏ β ((mulGrpβπ
) MndHom (mulGrpβπ))) |
74 | 73 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β πΏ β ((mulGrpβπ
) MndHom (mulGrpβπ))) |
75 | 48, 49, 23 | mhmmulg 19077 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΏ β ((mulGrpβπ
) MndHom (mulGrpβπ)) β§ (πβπ) β β0 β§ ((π΄ βΎ π½)βπ) β πΎ) β (πΏβ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) = ((πβπ)(.gβ(mulGrpβπ))(πΏβ((π΄ βΎ π½)βπ)))) |
76 | 74, 55, 60, 75 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β (πΏβ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) = ((πβπ)(.gβ(mulGrpβπ))(πΏβ((π΄ βΎ π½)βπ)))) |
77 | 58 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β (π΄ βΎ π½):π½βΆπΎ) |
78 | | simpr 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β π β π½) |
79 | 77, 78 | fvco3d 7003 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β ((πΏ β (π΄ βΎ π½))βπ) = (πΏβ((π΄ βΎ π½)βπ))) |
80 | 79 | oveq2d 7442 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)) = ((πβπ)(.gβ(mulGrpβπ))(πΏβ((π΄ βΎ π½)βπ)))) |
81 | 76, 80 | eqtr4d 2771 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β (πΏβ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) = ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))) |
82 | 81 | mpteq2dva 5252 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ (πΏβ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))) |
83 | 62, 82 | eqtrd 2768 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (πΏ β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))) |
84 | 83 | oveq2d 7442 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβπ)
Ξ£g (πΏ β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) = ((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))) |
85 | | eqid 2728 |
. . . . . . . . . . . . . . . . . 18
β’
(Baseβ(mulGrpβ(Scalarβπ))) =
(Baseβ(mulGrpβ(Scalarβπ))) |
86 | | eqid 2728 |
. . . . . . . . . . . . . . . . . 18
β’
(0gβ(mulGrpβ(Scalarβπ))) =
(0gβ(mulGrpβ(Scalarβπ))) |
87 | 68, 7 | eqeltrrd 2830 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (Scalarβπ) β CRing) |
88 | | eqid 2728 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(mulGrpβ(Scalarβπ)) = (mulGrpβ(Scalarβπ)) |
89 | 88 | crngmgp 20188 |
. . . . . . . . . . . . . . . . . . . 20
β’
((Scalarβπ)
β CRing β (mulGrpβ(Scalarβπ)) β CMnd) |
90 | 87, 89 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(mulGrpβ(Scalarβπ)) β CMnd) |
91 | 90 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(mulGrpβ(Scalarβπ)) β CMnd) |
92 | 22 | ringmgp 20186 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β Ring β
(mulGrpβπ) β
Mnd) |
93 | 9, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (mulGrpβπ) β Mnd) |
94 | 93 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(mulGrpβπ) β
Mnd) |
95 | 88, 22 | rhmmhm 20425 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΏ β ((Scalarβπ) RingHom π) β πΏ β ((mulGrpβ(Scalarβπ)) MndHom (mulGrpβπ))) |
96 | 67, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΏ β ((mulGrpβ(Scalarβπ)) MndHom (mulGrpβπ))) |
97 | 96 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β πΏ β
((mulGrpβ(Scalarβπ)) MndHom (mulGrpβπ))) |
98 | 68 | fveq2d 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (Baseβπ
) =
(Baseβ(Scalarβπ))) |
99 | 28, 98 | eqtrid 2780 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β πΎ = (Baseβ(Scalarβπ))) |
100 | 99 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β πΎ = (Baseβ(Scalarβπ))) |
101 | 61, 100 | eleqtrd 2831 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) β (Baseβ(Scalarβπ))) |
102 | | eqid 2728 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
103 | 88, 102 | mgpbas 20087 |
. . . . . . . . . . . . . . . . . . . 20
β’
(Baseβ(Scalarβπ)) =
(Baseβ(mulGrpβ(Scalarβπ))) |
104 | 101, 103 | eleqtrdi 2839 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) β
(Baseβ(mulGrpβ(Scalarβπ)))) |
105 | 104 | fmpttd 7130 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))):π½βΆ(Baseβ(mulGrpβ(Scalarβπ)))) |
106 | 54 | feqmptd 6972 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π = (π β π½ β¦ (πβπ))) |
107 | 13 | psrbagfsupp 21860 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β π finSupp 0) |
108 | 107 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π finSupp 0) |
109 | 106, 108 | eqbrtrrd 5176 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ (πβπ)) finSupp 0) |
110 | | eqid 2728 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(0gβ(mulGrpβπ
)) =
(0gβ(mulGrpβπ
)) |
111 | 48, 110, 49 | mulg0 19037 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β πΎ β
(0(.gβ(mulGrpβπ
))π) = (0gβ(mulGrpβπ
))) |
112 | 111 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β πΎ) β
(0(.gβ(mulGrpβπ
))π) = (0gβ(mulGrpβπ
))) |
113 | | fvexd 6917 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(0gβ(mulGrpβπ
)) β V) |
114 | 109, 112,
55, 60, 113 | fsuppssov1 9415 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) finSupp
(0gβ(mulGrpβπ
))) |
115 | | eqid 2728 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(1rβπ
) = (1rβπ
) |
116 | 47, 115 | ringidval 20130 |
. . . . . . . . . . . . . . . . . . . 20
β’
(1rβπ
) = (0gβ(mulGrpβπ
)) |
117 | 114, 116 | breqtrrdi 5194 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) finSupp (1rβπ
)) |
118 | 68 | fveq2d 6906 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1rβπ
) =
(1rβ(Scalarβπ))) |
119 | | eqid 2728 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
120 | 88, 119 | ringidval 20130 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(1rβ(Scalarβπ)) =
(0gβ(mulGrpβ(Scalarβπ))) |
121 | 118, 120 | eqtrdi 2784 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1rβπ
) =
(0gβ(mulGrpβ(Scalarβπ)))) |
122 | 121 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(1rβπ
) =
(0gβ(mulGrpβ(Scalarβπ)))) |
123 | 117, 122 | breqtrd 5178 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) finSupp
(0gβ(mulGrpβ(Scalarβπ)))) |
124 | 85, 86, 91, 94, 25, 97, 105, 123 | gsummhm 19900 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβπ)
Ξ£g (πΏ β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) = (πΏβ((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
125 | 84, 124 | eqtr3d 2770 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβπ)
Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))) = (πΏβ((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
126 | 125 | oveq2d 7442 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))) = (((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)(πΏβ((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))))) |
127 | 64 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π β AssAlg) |
128 | 101 | fmpttd 7130 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))):π½βΆ(Baseβ(Scalarβπ))) |
129 | 123, 120 | breqtrrdi 5194 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) finSupp
(1rβ(Scalarβπ))) |
130 | 103, 120,
91, 25, 128, 129 | gsumcl 19877 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) β (Baseβ(Scalarβπ))) |
131 | | eqid 2728 |
. . . . . . . . . . . . . . . . 17
β’ (
Β·π βπ) = ( Β·π
βπ) |
132 | 31, 65, 102, 1, 2, 131 | asclmul2 21827 |
. . . . . . . . . . . . . . . 16
β’ ((π β AssAlg β§
((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) β (Baseβ(Scalarβπ)) β§ ((((πΌ selectVars π
)βπ½)βπΉ)βπ) β (Baseβπ)) β (((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)(πΏβ((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) = (((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))( Β·π
βπ)((((πΌ selectVars π
)βπ½)βπΉ)βπ))) |
133 | 127, 130,
21, 132 | syl3anc 1368 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)(πΏβ((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) = (((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))( Β·π
βπ)((((πΌ selectVars π
)βπ½)βπΉ)βπ))) |
134 | 126, 133 | eqtrd 2768 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))) = (((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))( Β·π
βπ)((((πΌ selectVars π
)βπ½)βπΉ)βπ))) |
135 | 134 | fveq1d 6904 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))βπ) = ((((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))( Β·π
βπ)((((πΌ selectVars π
)βπ½)βπΉ)βπ))βπ)) |
136 | | eqid 2728 |
. . . . . . . . . . . . . 14
β’
(.rβπ
) = (.rβπ
) |
137 | | eqid 2728 |
. . . . . . . . . . . . . 14
β’ {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} = {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β
Fin} |
138 | 99 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β πΎ =
(Baseβ(Scalarβπ))) |
139 | 130, 138 | eleqtrrd 2832 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) β πΎ) |
140 | | simplr 767 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β
Fin}) |
141 | 3, 131, 28, 1, 136, 137, 139, 21, 140 | mplvscaval 21965 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))( Β·π
βπ)((((πΌ selectVars π
)βπ½)βπΉ)βπ))βπ) = (((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ))) |
142 | 135, 141 | eqtrd 2768 |
. . . . . . . . . . . 12
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))βπ) = (((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ))) |
143 | 142 | mpteq2dva 5252 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))βπ)) = (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)))) |
144 | 45, 143 | eqtrd 2768 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β ((π’ β (Baseβπ) β¦ (π’βπ)) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))) = (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)))) |
145 | 144 | oveq2d 7442 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π
Ξ£g
((π’ β
(Baseβπ) β¦
(π’βπ)) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))))) = (π
Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ))))) |
146 | 69 | fveq2d 6906 |
. . . . . . . . . . . . . . 15
β’ (π β
(mulGrpβ(Scalarβπ)) = (mulGrpβπ
)) |
147 | 146 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(mulGrpβ(Scalarβπ)) = (mulGrpβπ
)) |
148 | 147 | oveq1d 7441 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) = ((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) |
149 | 148 | oveq1d 7441 |
. . . . . . . . . . . 12
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) = (((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ))) |
150 | 7 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π
β CRing) |
151 | 148, 139 | eqeltrrd 2830 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβπ
)
Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) β πΎ) |
152 | 19 | ffvelcdmda 7099 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ)βπ) β (Baseβπ)) |
153 | 3, 28, 1, 137, 152 | mplelf 21947 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ)βπ):{π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}βΆπΎ) |
154 | 153 | ffvelcdmda 7099 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) β πΎ) |
155 | 154 | an32s 650 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) β πΎ) |
156 | 28, 136, 150, 151, 155 | crngcomd 20202 |
. . . . . . . . . . . 12
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((mulGrpβπ
)
Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) = ((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
157 | 149, 156 | eqtrd 2768 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) = ((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
158 | 157 | mpteq2dva 5252 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ))) = (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))))) |
159 | 158 | oveq2d 7442 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π
Ξ£g
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)))) = (π
Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))))) |
160 | 145, 159 | eqtrd 2768 |
. . . . . . . 8
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π
Ξ£g
((π’ β
(Baseβπ) β¦
(π’βπ)) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))))) = (π
Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))))) |
161 | 160 | oveq1d 7441 |
. . . . . . 7
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β ((π
Ξ£g
((π’ β
(Baseβπ) β¦
(π’βπ)) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))))(.rβπ
)((mulGrpβπ
) Ξ£g
(π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = ((π
Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
162 | | eqid 2728 |
. . . . . . . . . 10
β’ (π’ β (Baseβπ) β¦ (π’βπ)) = (π’ β (Baseβπ) β¦ (π’βπ)) |
163 | | fveq1 6901 |
. . . . . . . . . 10
β’ (π’ = (π Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))) β (π’βπ) = ((π Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))))βπ)) |
164 | | eqid 2728 |
. . . . . . . . . . . . 13
β’ (π½ eval π) = (π½ eval π) |
165 | 164, 11, 12, 13, 1, 22, 23, 2, 24, 8, 18, 37 | evlvvval 41837 |
. . . . . . . . . . . 12
β’ (π β (((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½))) = (π Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))))) |
166 | 164, 11, 12, 1, 24, 8, 18, 37 | evlcl 41836 |
. . . . . . . . . . . 12
β’ (π β (((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½))) β (Baseβπ)) |
167 | 165, 166 | eqeltrrd 2830 |
. . . . . . . . . . 11
β’ (π β (π Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))) β (Baseβπ)) |
168 | 167 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π Ξ£g
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))) β (Baseβπ)) |
169 | | fvexd 6917 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β ((π Ξ£g
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))))βπ) β V) |
170 | 162, 163,
168, 169 | fvmptd3 7033 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β ((π’ β (Baseβπ) β¦ (π’βπ))β(π Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))))) = ((π Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))))βπ)) |
171 | | eqid 2728 |
. . . . . . . . . 10
β’
(0gβπ) = (0gβπ) |
172 | 9 | ringcmnd 20227 |
. . . . . . . . . . 11
β’ (π β π β CMnd) |
173 | 172 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π β CMnd) |
174 | 7 | crnggrpd 20194 |
. . . . . . . . . . . 12
β’ (π β π
β Grp) |
175 | 174 | grpmndd 18910 |
. . . . . . . . . . 11
β’ (π β π
β Mnd) |
176 | 175 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π
β Mnd) |
177 | | ovex 7459 |
. . . . . . . . . . . 12
β’
(β0 βm π½) β V |
178 | 177 | rabex 5338 |
. . . . . . . . . . 11
β’ {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β
V |
179 | 178 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β
V) |
180 | 6 | adantr 479 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (πΌ β π½) β V) |
181 | 174 | adantr 479 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π
β Grp) |
182 | | simpr 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β
Fin}) |
183 | 3, 1, 137, 162, 180, 181, 182 | mplmapghm 41820 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π’ β (Baseβπ) β¦ (π’βπ)) β (π GrpHom π
)) |
184 | | ghmmhm 19187 |
. . . . . . . . . . 11
β’ ((π’ β (Baseβπ) β¦ (π’βπ)) β (π GrpHom π
) β (π’ β (Baseβπ) β¦ (π’βπ)) β (π MndHom π
)) |
185 | 183, 184 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π’ β (Baseβπ) β¦ (π’βπ)) β (π MndHom π
)) |
186 | 41 | fmpttd 7130 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))):{π β (β0
βm π½)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ)) |
187 | 24 | adantr 479 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π½ β V) |
188 | 8 | adantr 479 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π β CRing) |
189 | 18 | adantr 479 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(((πΌ selectVars π
)βπ½)βπΉ) β (Baseβπ)) |
190 | 37 | adantr 479 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (πΏ β (π΄ βΎ π½)) β ((Baseβπ) βm π½)) |
191 | 13, 11, 12, 1, 22, 23, 2, 187, 188, 189, 190 | evlvvvallem 41838 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))) finSupp (0gβπ)) |
192 | 1, 171, 173, 176, 179, 185, 186, 191 | gsummhm 19900 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π
Ξ£g
((π’ β
(Baseβπ) β¦
(π’βπ)) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))))) = ((π’ β (Baseβπ) β¦ (π’βπ))β(π Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))))) |
193 | 165 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½))) = (π Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))))) |
194 | 193 | fveq1d 6904 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
((((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½)))βπ) = ((π Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))))βπ)) |
195 | 170, 192,
194 | 3eqtr4rd 2779 |
. . . . . . . 8
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
((((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½)))βπ) = (π
Ξ£g ((π’ β (Baseβπ) β¦ (π’βπ)) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))))) |
196 | 195 | oveq1d 7441 |
. . . . . . 7
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(((((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½)))βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = ((π
Ξ£g ((π’ β (Baseβπ) β¦ (π’βπ)) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))))(.rβπ
)((mulGrpβπ
) Ξ£g
(π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
197 | | eqid 2728 |
. . . . . . . 8
β’
(0gβπ
) = (0gβπ
) |
198 | 32 | adantr 479 |
. . . . . . . 8
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π
β Ring) |
199 | 47 | crngmgp 20188 |
. . . . . . . . . . 11
β’ (π
β CRing β
(mulGrpβπ
) β
CMnd) |
200 | 7, 199 | syl 17 |
. . . . . . . . . 10
β’ (π β (mulGrpβπ
) β CMnd) |
201 | 200 | adantr 479 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(mulGrpβπ
) β
CMnd) |
202 | 51 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β (πΌ β π½)) β (mulGrpβπ
) β Mnd) |
203 | 137 | psrbagf 21858 |
. . . . . . . . . . . . 13
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β π:(πΌ β π½)βΆβ0) |
204 | 203 | adantl 480 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π:(πΌ β π½)βΆβ0) |
205 | 204 | ffvelcdmda 7099 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β (πΌ β π½)) β (πβπ) β
β0) |
206 | 57, 5 | fssresd 6769 |
. . . . . . . . . . . . 13
β’ (π β (π΄ βΎ (πΌ β π½)):(πΌ β π½)βΆπΎ) |
207 | 206 | adantr 479 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π΄ βΎ (πΌ β π½)):(πΌ β π½)βΆπΎ) |
208 | 207 | ffvelcdmda 7099 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β (πΌ β π½)) β ((π΄ βΎ (πΌ β π½))βπ) β πΎ) |
209 | 48, 49, 202, 205, 208 | mulgnn0cld 19057 |
. . . . . . . . . 10
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β (πΌ β π½)) β ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) β πΎ) |
210 | 209 | fmpttd 7130 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))):(πΌ β π½)βΆπΎ) |
211 | 204 | feqmptd 6972 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π = (π β (πΌ β π½) β¦ (πβπ))) |
212 | 137 | psrbagfsupp 21860 |
. . . . . . . . . . . 12
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β π finSupp 0) |
213 | 212 | adantl 480 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π finSupp 0) |
214 | 211, 213 | eqbrtrrd 5176 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β (πΌ β π½) β¦ (πβπ)) finSupp 0) |
215 | 48, 110, 49 | mulg0 19037 |
. . . . . . . . . . 11
β’ (π£ β πΎ β
(0(.gβ(mulGrpβπ
))π£) = (0gβ(mulGrpβπ
))) |
216 | 215 | adantl 480 |
. . . . . . . . . 10
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π£ β πΎ) β
(0(.gβ(mulGrpβπ
))π£) = (0gβ(mulGrpβπ
))) |
217 | | fvexd 6917 |
. . . . . . . . . 10
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β (πΌ β π½)) β (πβπ) β V) |
218 | | fvexd 6917 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(0gβ(mulGrpβπ
)) β V) |
219 | 214, 216,
217, 208, 218 | fsuppssov1 9415 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) finSupp
(0gβ(mulGrpβπ
))) |
220 | 48, 110, 201, 180, 210, 219 | gsumcl 19877 |
. . . . . . . 8
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
((mulGrpβπ
)
Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) β πΎ) |
221 | 32 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π
β Ring) |
222 | 28, 136, 221, 155, 151 | ringcld 20206 |
. . . . . . . 8
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) β πΎ) |
223 | 178 | mptex 7241 |
. . . . . . . . . . 11
β’ (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) β V |
224 | 223 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) β V) |
225 | | fvexd 6917 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(0gβπ
)
β V) |
226 | | funmpt 6596 |
. . . . . . . . . . 11
β’ Fun
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) |
227 | 226 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β Fun
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ))) |
228 | 11, 12, 171, 18, 8 | mplelsfi 21944 |
. . . . . . . . . . 11
β’ (π β (((πΌ selectVars π
)βπ½)βπΉ) finSupp (0gβπ)) |
229 | 228 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(((πΌ selectVars π
)βπ½)βπΉ) finSupp (0gβπ)) |
230 | | ssidd 4005 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ) supp (0gβπ)) β ((((πΌ selectVars π
)βπ½)βπΉ) supp (0gβπ))) |
231 | | fvexd 6917 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(0gβπ)
β V) |
232 | 20, 230, 179, 231 | suppssr 8207 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β ({π β (β0
βm π½)
β£ (β‘π β β) β Fin} β
((((πΌ selectVars π
)βπ½)βπΉ) supp (0gβπ)))) β ((((πΌ selectVars π
)βπ½)βπΉ)βπ) = (0gβπ)) |
233 | 232 | fveq1d 6904 |
. . . . . . . . . . . 12
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β ({π β (β0
βm π½)
β£ (β‘π β β) β Fin} β
((((πΌ selectVars π
)βπ½)βπΉ) supp (0gβπ)))) β (((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) = ((0gβπ)βπ)) |
234 | 3, 137, 197, 171, 6, 174 | mpl0 21955 |
. . . . . . . . . . . . . . . 16
β’ (π β (0gβπ) = ({π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} Γ
{(0gβπ
)})) |
235 | 234 | adantr 479 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(0gβπ) =
({π β
(β0 βm (πΌ β π½)) β£ (β‘π β β) β Fin} Γ
{(0gβπ
)})) |
236 | 235 | fveq1d 6904 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
((0gβπ)βπ) = (({π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} Γ
{(0gβπ
)})βπ)) |
237 | | fvex 6915 |
. . . . . . . . . . . . . . . 16
β’
(0gβπ
) β V |
238 | 237 | fvconst2 7222 |
. . . . . . . . . . . . . . 15
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β (({π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} Γ
{(0gβπ
)})βπ) = (0gβπ
)) |
239 | 238 | adantl 480 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(({π β
(β0 βm (πΌ β π½)) β£ (β‘π β β) β Fin} Γ
{(0gβπ
)})βπ) = (0gβπ
)) |
240 | 236, 239 | eqtrd 2768 |
. . . . . . . . . . . . 13
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
((0gβπ)βπ) = (0gβπ
)) |
241 | 240 | adantr 479 |
. . . . . . . . . . . 12
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β ({π β (β0
βm π½)
β£ (β‘π β β) β Fin} β
((((πΌ selectVars π
)βπ½)βπΉ) supp (0gβπ)))) β
((0gβπ)βπ) = (0gβπ
)) |
242 | 233, 241 | eqtrd 2768 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β ({π β (β0
βm π½)
β£ (β‘π β β) β Fin} β
((((πΌ selectVars π
)βπ½)βπΉ) supp (0gβπ)))) β (((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) = (0gβπ
)) |
243 | 242, 179 | suppss2 8212 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β ((π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) supp (0gβπ
)) β ((((πΌ selectVars π
)βπ½)βπΉ) supp (0gβπ))) |
244 | 224, 225,
227, 229, 243 | fsuppsssuppgd 9413 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) finSupp (0gβπ
)) |
245 | 32 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π£ β πΎ) β π
β Ring) |
246 | | simpr 483 |
. . . . . . . . . 10
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π£ β πΎ) β π£ β πΎ) |
247 | 28, 136, 197, 245, 246 | ringlzd 20238 |
. . . . . . . . 9
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π£ β πΎ) β ((0gβπ
)(.rβπ
)π£) = (0gβπ
)) |
248 | 244, 247,
155, 151, 225 | fsuppssov1 9415 |
. . . . . . . 8
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) finSupp (0gβπ
)) |
249 | 28, 197, 136, 198, 179, 220, 222, 248 | gsummulc1 20259 |
. . . . . . 7
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π
Ξ£g
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))) = ((π
Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
250 | 161, 196,
249 | 3eqtr4d 2778 |
. . . . . 6
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(((((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½)))βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = (π
Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))))) |
251 | | fveq2 6902 |
. . . . . . . . . . . . . 14
β’ (π = π β ((((πΌ selectVars π
)βπ½)βπΉ)βπ) = ((((πΌ selectVars π
)βπ½)βπΉ)βπ)) |
252 | 251 | adantl 480 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = π) β ((((πΌ selectVars π
)βπ½)βπΉ)βπ) = ((((πΌ selectVars π
)βπ½)βπΉ)βπ)) |
253 | | simpl 481 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = π) β π = π) |
254 | 252, 253 | fveq12d 6909 |
. . . . . . . . . . . 12
β’ ((π = π β§ π = π) β (((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) = (((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) |
255 | | fveq1 6901 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πβπ) = (πβπ)) |
256 | 255 | adantl 480 |
. . . . . . . . . . . . . . 15
β’ ((π = π β§ π = π) β (πβπ) = (πβπ)) |
257 | 256 | oveq1d 7441 |
. . . . . . . . . . . . . 14
β’ ((π = π β§ π = π) β ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) |
258 | 257 | mpteq2dv 5254 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = π) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) |
259 | 258 | oveq2d 7442 |
. . . . . . . . . . . 12
β’ ((π = π β§ π = π) β ((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) = ((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) |
260 | 254, 259 | oveq12d 7444 |
. . . . . . . . . . 11
β’ ((π = π β§ π = π) β ((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) = ((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
261 | | fveq1 6901 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβπ) = (πβπ)) |
262 | 261 | adantr 479 |
. . . . . . . . . . . . . 14
β’ ((π = π β§ π = π) β (πβπ) = (πβπ)) |
263 | 262 | oveq1d 7441 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = π) β ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) = ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) |
264 | 263 | mpteq2dv 5254 |
. . . . . . . . . . . 12
β’ ((π = π β§ π = π) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) |
265 | 264 | oveq2d 7442 |
. . . . . . . . . . 11
β’ ((π = π β§ π = π) β ((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) = ((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) |
266 | 260, 265 | oveq12d 7444 |
. . . . . . . . . 10
β’ ((π = π β§ π = π) β (((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = (((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
267 | | eqid 2728 |
. . . . . . . . . 10
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) = (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
268 | | ovex 7459 |
. . . . . . . . . 10
β’
(((((((πΌ selectVars
π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) β V |
269 | 266, 267,
268 | ovmpoa 7582 |
. . . . . . . . 9
β’ ((π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π(π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))π) = (((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
270 | 269 | adantll 712 |
. . . . . . . 8
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π(π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))π) = (((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
271 | 270 | mpteq2dva 5252 |
. . . . . . 7
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π(π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))π)) = (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))) |
272 | 271 | oveq2d 7442 |
. . . . . 6
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π
Ξ£g
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π(π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))π))) = (π
Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))))) |
273 | 250, 272 | eqtr4d 2771 |
. . . . 5
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(((((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½)))βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = (π
Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π(π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))π)))) |
274 | 273 | mpteq2dva 5252 |
. . . 4
β’ (π β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β¦
(((((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½)))βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) = (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β¦ (π
Ξ£g
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π(π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))π))))) |
275 | 274 | oveq2d 7442 |
. . 3
β’ (π β (π
Ξ£g (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β¦
(((((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½)))βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))) = (π
Ξ£g (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β¦ (π
Ξ£g
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π(π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))π)))))) |
276 | 32 | ringcmnd 20227 |
. . . . 5
β’ (π β π
β CMnd) |
277 | | ovex 7459 |
. . . . . . 7
β’
(β0 βm πΌ) β V |
278 | 277 | rabex 5338 |
. . . . . 6
β’ {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β
V |
279 | 278 | a1i 11 |
. . . . 5
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β
V) |
280 | 32 | adantr 479 |
. . . . . . 7
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π
β Ring) |
281 | 19 | adantr 479 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (((πΌ selectVars π
)βπ½)βπΉ):{π β (β0
βm π½)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ)) |
282 | | eqid 2728 |
. . . . . . . . . . . 12
β’ {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} = {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
283 | 4 | adantr 479 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β πΌ β π) |
284 | 16 | adantr 479 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π½ β πΌ) |
285 | | simpr 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π β {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
286 | 282, 13, 283, 284, 285 | psrbagres 41807 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βΎ π½) β {π β (β0
βm π½)
β£ (β‘π β β) β
Fin}) |
287 | 281, 286 | ffvelcdmd 7100 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½)) β (Baseβπ)) |
288 | 3, 28, 1, 137, 287 | mplelf 21947 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½)):{π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}βΆπΎ) |
289 | | difssd 4133 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (πΌ β π½) β πΌ) |
290 | 282, 137,
283, 289, 285 | psrbagres 41807 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βΎ (πΌ β π½)) β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β
Fin}) |
291 | 288, 290 | ffvelcdmd 7100 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½))) β πΎ) |
292 | 200 | adantr 479 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(mulGrpβπ
) β
CMnd) |
293 | 24 | adantr 479 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π½ β V) |
294 | 51 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β (mulGrpβπ
) β Mnd) |
295 | 282 | psrbagf 21858 |
. . . . . . . . . . . . . 14
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β π:πΌβΆβ0) |
296 | 295 | adantl 480 |
. . . . . . . . . . . . 13
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π:πΌβΆβ0) |
297 | 296, 284 | fssresd 6769 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βΎ π½):π½βΆβ0) |
298 | 297 | ffvelcdmda 7099 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β ((π βΎ π½)βπ) β
β0) |
299 | 58 | ffvelcdmda 7099 |
. . . . . . . . . . . 12
β’ ((π β§ π β π½) β ((π΄ βΎ π½)βπ) β πΎ) |
300 | 299 | adantlr 713 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β ((π΄ βΎ π½)βπ) β πΎ) |
301 | 48, 49, 294, 298, 300 | mulgnn0cld 19057 |
. . . . . . . . . 10
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) β πΎ) |
302 | 301 | fmpttd 7130 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))):π½βΆπΎ) |
303 | 24 | mptexd 7242 |
. . . . . . . . . . 11
β’ (π β (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) β V) |
304 | 303 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) β V) |
305 | | fvexd 6917 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(0gβ(mulGrpβπ
)) β V) |
306 | | funmpt 6596 |
. . . . . . . . . . 11
β’ Fun
(π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) |
307 | 306 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β Fun
(π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) |
308 | 282 | psrbagfsupp 21860 |
. . . . . . . . . . . 12
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β π finSupp 0) |
309 | 308 | adantl 480 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π finSupp 0) |
310 | | 0zd 12608 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β 0 β
β€) |
311 | 309, 310 | fsuppres 9424 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βΎ π½) finSupp 0) |
312 | | ssidd 4005 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π βΎ π½) supp 0) β ((π βΎ π½) supp 0)) |
313 | 297, 312,
293, 310 | suppssr 8207 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (π½ β ((π βΎ π½) supp 0))) β ((π βΎ π½)βπ) = 0) |
314 | 313 | oveq1d 7441 |
. . . . . . . . . . . 12
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (π½ β ((π βΎ π½) supp 0))) β (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) =
(0(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) |
315 | | eldifi 4127 |
. . . . . . . . . . . . 13
β’ (π β (π½ β ((π βΎ π½) supp 0)) β π β π½) |
316 | 48, 110, 49 | mulg0 19037 |
. . . . . . . . . . . . . 14
β’ (((π΄ βΎ π½)βπ) β πΎ β
(0(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = (0gβ(mulGrpβπ
))) |
317 | 300, 316 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β
(0(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = (0gβ(mulGrpβπ
))) |
318 | 315, 317 | sylan2 591 |
. . . . . . . . . . . 12
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (π½ β ((π βΎ π½) supp 0))) β
(0(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = (0gβ(mulGrpβπ
))) |
319 | 314, 318 | eqtrd 2768 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (π½ β ((π βΎ π½) supp 0))) β (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = (0gβ(mulGrpβπ
))) |
320 | 319, 293 | suppss2 8212 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) supp
(0gβ(mulGrpβπ
))) β ((π βΎ π½) supp 0)) |
321 | 304, 305,
307, 311, 320 | fsuppsssuppgd 9413 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) finSupp
(0gβ(mulGrpβπ
))) |
322 | 48, 110, 292, 293, 302, 321 | gsumcl 19877 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((mulGrpβπ
)
Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) β πΎ) |
323 | 28, 136, 280, 291, 322 | ringcld 20206 |
. . . . . . 7
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) β πΎ) |
324 | 6 | adantr 479 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (πΌ β π½) β V) |
325 | 51 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β (mulGrpβπ
) β Mnd) |
326 | 296, 289 | fssresd 6769 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βΎ (πΌ β π½)):(πΌ β π½)βΆβ0) |
327 | 326 | ffvelcdmda 7099 |
. . . . . . . . . 10
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β ((π βΎ (πΌ β π½))βπ) β
β0) |
328 | 206 | ffvelcdmda 7099 |
. . . . . . . . . . 11
β’ ((π β§ π β (πΌ β π½)) β ((π΄ βΎ (πΌ β π½))βπ) β πΎ) |
329 | 328 | adantlr 713 |
. . . . . . . . . 10
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β ((π΄ βΎ (πΌ β π½))βπ) β πΎ) |
330 | 48, 49, 325, 327, 329 | mulgnn0cld 19057 |
. . . . . . . . 9
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) β πΎ) |
331 | 330 | fmpttd 7130 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))):(πΌ β π½)βΆπΎ) |
332 | 324 | mptexd 7242 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) β V) |
333 | | funmpt 6596 |
. . . . . . . . . 10
β’ Fun
(π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) |
334 | 333 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β Fun
(π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) |
335 | 309, 310 | fsuppres 9424 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βΎ (πΌ β π½)) finSupp 0) |
336 | | ssidd 4005 |
. . . . . . . . . . . . 13
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π βΎ (πΌ β π½)) supp 0) β ((π βΎ (πΌ β π½)) supp 0)) |
337 | 326, 336,
324, 310 | suppssr 8207 |
. . . . . . . . . . . 12
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β ((πΌ β π½) β ((π βΎ (πΌ β π½)) supp 0))) β ((π βΎ (πΌ β π½))βπ) = 0) |
338 | 337 | oveq1d 7441 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β ((πΌ β π½) β ((π βΎ (πΌ β π½)) supp 0))) β (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) =
(0(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) |
339 | | eldifi 4127 |
. . . . . . . . . . . . 13
β’ (π β ((πΌ β π½) β ((π βΎ (πΌ β π½)) supp 0)) β π β (πΌ β π½)) |
340 | 339, 329 | sylan2 591 |
. . . . . . . . . . . 12
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β ((πΌ β π½) β ((π βΎ (πΌ β π½)) supp 0))) β ((π΄ βΎ (πΌ β π½))βπ) β πΎ) |
341 | 48, 110, 49 | mulg0 19037 |
. . . . . . . . . . . 12
β’ (((π΄ βΎ (πΌ β π½))βπ) β πΎ β
(0(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) = (0gβ(mulGrpβπ
))) |
342 | 340, 341 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β ((πΌ β π½) β ((π βΎ (πΌ β π½)) supp 0))) β
(0(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) = (0gβ(mulGrpβπ
))) |
343 | 338, 342 | eqtrd 2768 |
. . . . . . . . . 10
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β ((πΌ β π½) β ((π βΎ (πΌ β π½)) supp 0))) β (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) = (0gβ(mulGrpβπ
))) |
344 | 343, 324 | suppss2 8212 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) supp
(0gβ(mulGrpβπ
))) β ((π βΎ (πΌ β π½)) supp 0)) |
345 | 332, 305,
334, 335, 344 | fsuppsssuppgd 9413 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) finSupp
(0gβ(mulGrpβπ
))) |
346 | 48, 110, 292, 324, 331, 345 | gsumcl 19877 |
. . . . . . 7
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((mulGrpβπ
)
Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) β πΎ) |
347 | 28, 136, 280, 323, 346 | ringcld 20206 |
. . . . . 6
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) β πΎ) |
348 | 347 | fmpttd 7130 |
. . . . 5
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))):{β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}βΆπΎ) |
349 | 7 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π
β CRing) |
350 | 17 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β πΉ β π΅) |
351 | 282, 14, 15, 283, 349, 284, 350, 285 | selvvvval 41849 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½))) = (πΉβπ)) |
352 | 351 | mpteq2dva 5252 |
. . . . . . . 8
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))) = (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (πΉβπ))) |
353 | | eqid 2728 |
. . . . . . . . . . 11
β’
(Baseβπ
) =
(Baseβπ
) |
354 | 14, 353, 15, 282, 17 | mplelf 21947 |
. . . . . . . . . 10
β’ (π β πΉ:{β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}βΆ(Baseβπ
)) |
355 | 354 | feqmptd 6972 |
. . . . . . . . 9
β’ (π β πΉ = (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (πΉβπ))) |
356 | 14, 15, 197, 17, 7 | mplelsfi 21944 |
. . . . . . . . 9
β’ (π β πΉ finSupp (0gβπ
)) |
357 | 355, 356 | eqbrtrrd 5176 |
. . . . . . . 8
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (πΉβπ)) finSupp (0gβπ
)) |
358 | 352, 357 | eqbrtrd 5174 |
. . . . . . 7
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))) finSupp (0gβπ
)) |
359 | 32 | adantr 479 |
. . . . . . . 8
β’ ((π β§ π£ β πΎ) β π
β Ring) |
360 | | simpr 483 |
. . . . . . . 8
β’ ((π β§ π£ β πΎ) β π£ β πΎ) |
361 | 28, 136, 197, 359, 360 | ringlzd 20238 |
. . . . . . 7
β’ ((π β§ π£ β πΎ) β ((0gβπ
)(.rβπ
)π£) = (0gβπ
)) |
362 | | fvexd 6917 |
. . . . . . 7
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½))) β V) |
363 | | fvexd 6917 |
. . . . . . 7
β’ (π β (0gβπ
) β V) |
364 | 358, 361,
362, 322, 363 | fsuppssov1 9415 |
. . . . . 6
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) finSupp (0gβπ
)) |
365 | | ovexd 7461 |
. . . . . 6
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) β V) |
366 | 364, 361,
365, 346, 363 | fsuppssov1 9415 |
. . . . 5
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) finSupp (0gβπ
)) |
367 | | eqid 2728 |
. . . . . 6
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π)) = (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π)) |
368 | 282, 13, 137, 367, 4, 16 | evlselvlem 41850 |
. . . . 5
β’ (π β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π)):({π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} Γ {π β (β0
βm π½)
β£ (β‘π β β) β Fin})β1-1-ontoβ{β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
369 | 28, 197, 276, 279, 348, 366, 368 | gsumf1o 19878 |
. . . 4
β’ (π β (π
Ξ£g (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))) = (π
Ξ£g ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π))))) |
370 | 137 | psrbagf 21858 |
. . . . . . . . . 10
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β π:(πΌ β π½)βΆβ0) |
371 | 370 | ad2antrl 726 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π:(πΌ β π½)βΆβ0) |
372 | 13 | psrbagf 21858 |
. . . . . . . . . 10
β’ (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β π:π½βΆβ0) |
373 | 372 | ad2antll 727 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π:π½βΆβ0) |
374 | | disjdifr 4476 |
. . . . . . . . . 10
β’ ((πΌ β π½) β© π½) = β
|
375 | 374 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((πΌ β π½) β© π½) = β
) |
376 | 371, 373,
375 | fun2d 6766 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π βͺ π):((πΌ β π½) βͺ π½)βΆβ0) |
377 | | undifr 4486 |
. . . . . . . . . . 11
β’ (π½ β πΌ β ((πΌ β π½) βͺ π½) = πΌ) |
378 | 16, 377 | sylib 217 |
. . . . . . . . . 10
β’ (π β ((πΌ β π½) βͺ π½) = πΌ) |
379 | 378 | adantr 479 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((πΌ β π½) βͺ π½) = πΌ) |
380 | 379 | feq2d 6713 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((π βͺ π):((πΌ β π½) βͺ π½)βΆβ0 β (π βͺ π):πΌβΆβ0)) |
381 | 376, 380 | mpbid 231 |
. . . . . . 7
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π βͺ π):πΌβΆβ0) |
382 | | vex 3477 |
. . . . . . . . . . 11
β’ π β V |
383 | | vex 3477 |
. . . . . . . . . . 11
β’ π β V |
384 | 382, 383 | unex 7754 |
. . . . . . . . . 10
β’ (π βͺ π) β V |
385 | 384 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π βͺ π) β V) |
386 | | 0zd 12608 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β 0
β β€) |
387 | 381 | ffund 6731 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β Fun
(π βͺ π)) |
388 | 137 | psrbagfsupp 21860 |
. . . . . . . . . . 11
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β π finSupp 0) |
389 | 388 | ad2antrl 726 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π finSupp 0) |
390 | 13 | psrbagfsupp 21860 |
. . . . . . . . . . 11
β’ (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β π finSupp 0) |
391 | 390 | ad2antll 727 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π finSupp 0) |
392 | 389, 391 | fsuppun 9418 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((π βͺ π) supp 0) β
Fin) |
393 | 385, 386,
387, 392 | isfsuppd 9398 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π βͺ π) finSupp 0) |
394 | | fcdmnn0fsuppg 12569 |
. . . . . . . . 9
β’ (((π βͺ π) β V β§ (π βͺ π):πΌβΆβ0) β ((π βͺ π) finSupp 0 β (β‘(π βͺ π) β β) β
Fin)) |
395 | 385, 381,
394 | syl2anc 582 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((π βͺ π) finSupp 0 β (β‘(π βͺ π) β β) β
Fin)) |
396 | 393, 395 | mpbid 231 |
. . . . . . 7
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (β‘(π βͺ π) β β) β
Fin) |
397 | 4 | adantr 479 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β πΌ β π) |
398 | 282 | psrbag 21857 |
. . . . . . . 8
β’ (πΌ β π β ((π βͺ π) β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β ((π βͺ π):πΌβΆβ0 β§ (β‘(π βͺ π) β β) β
Fin))) |
399 | 397, 398 | syl 17 |
. . . . . . 7
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((π βͺ π) β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β ((π βͺ π):πΌβΆβ0 β§ (β‘(π βͺ π) β β) β
Fin))) |
400 | 381, 396,
399 | mpbir2and 711 |
. . . . . 6
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π βͺ π) β {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
401 | | eqidd 2729 |
. . . . . 6
β’ (π β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π)) = (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π))) |
402 | | eqidd 2729 |
. . . . . 6
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) = (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))) |
403 | | reseq1 5983 |
. . . . . . . . . . . 12
β’ (π = (π βͺ π) β (π βΎ π½) = ((π βͺ π) βΎ π½)) |
404 | 403 | fveq2d 6906 |
. . . . . . . . . . 11
β’ (π = (π βͺ π) β ((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½)) = ((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½))) |
405 | | reseq1 5983 |
. . . . . . . . . . 11
β’ (π = (π βͺ π) β (π βΎ (πΌ β π½)) = ((π βͺ π) βΎ (πΌ β π½))) |
406 | 404, 405 | fveq12d 6909 |
. . . . . . . . . 10
β’ (π = (π βͺ π) β (((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½))) = (((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½))β((π βͺ π) βΎ (πΌ β π½)))) |
407 | 403 | fveq1d 6904 |
. . . . . . . . . . . . 13
β’ (π = (π βͺ π) β ((π βΎ π½)βπ) = (((π βͺ π) βΎ π½)βπ)) |
408 | 407 | oveq1d 7441 |
. . . . . . . . . . . 12
β’ (π = (π βͺ π) β (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) |
409 | 408 | mpteq2dv 5254 |
. . . . . . . . . . 11
β’ (π = (π βͺ π) β (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) = (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) |
410 | 409 | oveq2d 7442 |
. . . . . . . . . 10
β’ (π = (π βͺ π) β ((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) = ((mulGrpβπ
) Ξ£g (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) |
411 | 406, 410 | oveq12d 7444 |
. . . . . . . . 9
β’ (π = (π βͺ π) β ((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) = ((((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½))β((π βͺ π) βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
412 | 405 | fveq1d 6904 |
. . . . . . . . . . . 12
β’ (π = (π βͺ π) β ((π βΎ (πΌ β π½))βπ) = (((π βͺ π) βΎ (πΌ β π½))βπ)) |
413 | 412 | oveq1d 7441 |
. . . . . . . . . . 11
β’ (π = (π βͺ π) β (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) = ((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) |
414 | 413 | mpteq2dv 5254 |
. . . . . . . . . 10
β’ (π = (π βͺ π) β (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) = (π β (πΌ β π½) β¦ ((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) |
415 | 414 | oveq2d 7442 |
. . . . . . . . 9
β’ (π = (π βͺ π) β ((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) = ((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) |
416 | 411, 415 | oveq12d 7444 |
. . . . . . . 8
β’ (π = (π βͺ π) β (((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = (((((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½))β((π βͺ π) βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
417 | 384, 416 | csbie 3930 |
. . . . . . 7
β’
β¦(π
βͺ π) / πβ¦(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = (((((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½))β((π βͺ π) βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) |
418 | 370 | ffnd 6728 |
. . . . . . . . . . . . 13
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β π Fn (πΌ β π½)) |
419 | 418 | ad2antrl 726 |
. . . . . . . . . . . 12
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π Fn (πΌ β π½)) |
420 | 373 | ffnd 6728 |
. . . . . . . . . . . 12
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π Fn π½) |
421 | | fnunres2 6672 |
. . . . . . . . . . . 12
β’ ((π Fn (πΌ β π½) β§ π Fn π½ β§ ((πΌ β π½) β© π½) = β
) β ((π βͺ π) βΎ π½) = π) |
422 | 419, 420,
375, 421 | syl3anc 1368 |
. . . . . . . . . . 11
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((π βͺ π) βΎ π½) = π) |
423 | 422 | fveq2d 6906 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½)) = ((((πΌ selectVars π
)βπ½)βπΉ)βπ)) |
424 | | fnunres1 6671 |
. . . . . . . . . . 11
β’ ((π Fn (πΌ β π½) β§ π Fn π½ β§ ((πΌ β π½) β© π½) = β
) β ((π βͺ π) βΎ (πΌ β π½)) = π) |
425 | 419, 420,
375, 424 | syl3anc 1368 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((π βͺ π) βΎ (πΌ β π½)) = π) |
426 | 423, 425 | fveq12d 6909 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
(((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½))β((π βͺ π) βΎ (πΌ β π½))) = (((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) |
427 | 422 | fveq1d 6904 |
. . . . . . . . . . . 12
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
(((π βͺ π) βΎ π½)βπ) = (πβπ)) |
428 | 427 | oveq1d 7441 |
. . . . . . . . . . 11
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) |
429 | 428 | mpteq2dv 5254 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) |
430 | 429 | oveq2d 7442 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((mulGrpβπ
)
Ξ£g (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) = ((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) |
431 | 426, 430 | oveq12d 7444 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½))β((π βͺ π) βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) = ((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
432 | 425 | fveq1d 6904 |
. . . . . . . . . . 11
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
(((π βͺ π) βΎ (πΌ β π½))βπ) = (πβπ)) |
433 | 432 | oveq1d 7441 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) = ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) |
434 | 433 | mpteq2dv 5254 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π β (πΌ β π½) β¦ ((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) |
435 | 434 | oveq2d 7442 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((mulGrpβπ
)
Ξ£g (π β (πΌ β π½) β¦ ((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) = ((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) |
436 | 431, 435 | oveq12d 7444 |
. . . . . . 7
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
(((((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½))β((π βͺ π) βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = (((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
437 | 417, 436 | eqtrid 2780 |
. . . . . 6
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
β¦(π βͺ
π) / πβ¦(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = (((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
438 | 400, 401,
402, 437 | fmpocos 41756 |
. . . . 5
β’ (π β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π))) = (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))) |
439 | 438 | oveq2d 7442 |
. . . 4
β’ (π β (π
Ξ£g ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π)))) = (π
Ξ£g (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))))) |
440 | | ovex 7459 |
. . . . . . 7
β’
(β0 βm (πΌ β π½)) β V |
441 | 440 | rabex 5338 |
. . . . . 6
β’ {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β
V |
442 | 441 | a1i 11 |
. . . . 5
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β
V) |
443 | 178 | a1i 11 |
. . . . 5
β’ (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β
V) |
444 | 32 | adantr 479 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π
β Ring) |
445 | 19 | ffvelcdmda 7099 |
. . . . . . . . . . . . 13
β’ ((π β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ)βπ) β (Baseβπ)) |
446 | 3, 28, 1, 137, 445 | mplelf 21947 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ)βπ):{π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}βΆπΎ) |
447 | 446 | ffvelcdmda 7099 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) β πΎ) |
448 | 447 | an32s 650 |
. . . . . . . . . 10
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) β πΎ) |
449 | 448 | anasss 465 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) β πΎ) |
450 | 24 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π½ β V) |
451 | 7 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π
β CRing) |
452 | 36 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π΄ βΎ π½) β (πΎ βm π½)) |
453 | | simprr 771 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π β {π β (β0
βm π½)
β£ (β‘π β β) β
Fin}) |
454 | 13, 28, 47, 49, 450, 451, 452, 453 | evlsvvvallem 41825 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((mulGrpβπ
)
Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) β πΎ) |
455 | 28, 136, 444, 449, 454 | ringcld 20206 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) β πΎ) |
456 | 6 | adantr 479 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (πΌ β π½) β V) |
457 | 35, 5 | elmapssresd 41763 |
. . . . . . . . . 10
β’ (π β (π΄ βΎ (πΌ β π½)) β (πΎ βm (πΌ β π½))) |
458 | 457 | adantr 479 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π΄ βΎ (πΌ β π½)) β (πΎ βm (πΌ β π½))) |
459 | | simprl 769 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β
Fin}) |
460 | 137, 28, 47, 49, 456, 451, 458, 459 | evlsvvvallem 41825 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((mulGrpβπ
)
Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) β πΎ) |
461 | 28, 136, 444, 455, 460 | ringcld 20206 |
. . . . . . 7
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) β πΎ) |
462 | 461 | ralrimivva 3198 |
. . . . . 6
β’ (π β βπ β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}βπ β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} (((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) β πΎ) |
463 | 267 | fmpo 8078 |
. . . . . 6
β’
(βπ β
{π β
(β0 βm (πΌ β π½)) β£ (β‘π β β) β Fin}βπ β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} (((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) β πΎ β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))):({π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} Γ {π β (β0
βm π½)
β£ (β‘π β β) β Fin})βΆπΎ) |
464 | 462, 463 | sylib 217 |
. . . . 5
β’ (π β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))):({π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} Γ {π β (β0
βm π½)
β£ (β‘π β β) β Fin})βΆπΎ) |
465 | | f1of1 6843 |
. . . . . . . 8
β’ ((π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π)):({π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} Γ {π β (β0
βm π½)
β£ (β‘π β β) β Fin})β1-1-ontoβ{β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π)):({π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} Γ {π β (β0
βm π½)
β£ (β‘π β β) β Fin})β1-1β{β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
466 | 368, 465 | syl 17 |
. . . . . . 7
β’ (π β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π)):({π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} Γ {π β (β0
βm π½)
β£ (β‘π β β) β Fin})β1-1β{β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
467 | 278 | mptex 7241 |
. . . . . . . 8
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) β V |
468 | 467 | a1i 11 |
. . . . . . 7
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) β V) |
469 | 366, 466,
363, 468 | fsuppco 9433 |
. . . . . 6
β’ (π β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π))) finSupp (0gβπ
)) |
470 | 438, 469 | eqbrtrrd 5176 |
. . . . 5
β’ (π β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) finSupp (0gβπ
)) |
471 | 28, 197, 276, 442, 443, 464, 470 | gsumxp 19938 |
. . . 4
β’ (π β (π
Ξ£g (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))) = (π
Ξ£g (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β¦ (π
Ξ£g
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π(π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))π)))))) |
472 | 369, 439,
471 | 3eqtrd 2772 |
. . 3
β’ (π β (π
Ξ£g (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))) = (π
Ξ£g (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β¦ (π
Ξ£g
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π(π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))π)))))) |
473 | 28, 136, 280, 291, 322, 346 | ringassd 20204 |
. . . . . 6
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = ((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)(((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))) |
474 | 47, 136 | mgpplusg 20085 |
. . . . . . . . 9
β’
(.rβπ
) = (+gβ(mulGrpβπ
)) |
475 | 51 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β (mulGrpβπ
) β Mnd) |
476 | 296 | ffvelcdmda 7099 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β (πβπ) β
β0) |
477 | 57 | adantr 479 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π΄:πΌβΆπΎ) |
478 | 477 | ffvelcdmda 7099 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β (π΄βπ) β πΎ) |
479 | 48, 49, 475, 476, 478 | mulgnn0cld 19057 |
. . . . . . . . . 10
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)) β πΎ) |
480 | 479 | fmpttd 7130 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))):πΌβΆπΎ) |
481 | 296 | feqmptd 6972 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π = (π β πΌ β¦ (πβπ))) |
482 | 481, 309 | eqbrtrrd 5176 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β πΌ β¦ (πβπ)) finSupp 0) |
483 | 111 | adantl 480 |
. . . . . . . . . 10
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΎ) β
(0(.gβ(mulGrpβπ
))π) = (0gβ(mulGrpβπ
))) |
484 | 482, 483,
476, 478, 305 | fsuppssov1 9415 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) finSupp
(0gβ(mulGrpβπ
))) |
485 | | disjdif 4475 |
. . . . . . . . . 10
β’ (π½ β© (πΌ β π½)) = β
|
486 | 485 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π½ β© (πΌ β π½)) = β
) |
487 | | undif 4485 |
. . . . . . . . . . . 12
β’ (π½ β πΌ β (π½ βͺ (πΌ β π½)) = πΌ) |
488 | 16, 487 | sylib 217 |
. . . . . . . . . . 11
β’ (π β (π½ βͺ (πΌ β π½)) = πΌ) |
489 | 488 | eqcomd 2734 |
. . . . . . . . . 10
β’ (π β πΌ = (π½ βͺ (πΌ β π½))) |
490 | 489 | adantr 479 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β πΌ = (π½ βͺ (πΌ β π½))) |
491 | 48, 110, 474, 292, 283, 480, 484, 486, 490 | gsumsplit 19890 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((mulGrpβπ
)
Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))) = (((mulGrpβπ
) Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ π½))(.rβπ
)((mulGrpβπ
) Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ (πΌ β π½))))) |
492 | 284 | resmptd 6049 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ π½) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))) |
493 | | fveq2 6902 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβπ) = (πβπ)) |
494 | | fveq2 6902 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΄βπ) = (π΄βπ)) |
495 | 493, 494 | oveq12d 7444 |
. . . . . . . . . . . . 13
β’ (π = π β ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)) = ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) |
496 | 495 | cbvmptv 5265 |
. . . . . . . . . . . 12
β’ (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) |
497 | | simpr 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β π β π½) |
498 | 497 | fvresd 6922 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β ((π βΎ π½)βπ) = (πβπ)) |
499 | 497 | fvresd 6922 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β ((π΄ βΎ π½)βπ) = (π΄βπ)) |
500 | 498, 499 | oveq12d 7444 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) |
501 | 500 | eqcomd 2734 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)) = (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) |
502 | 501 | mpteq2dva 5252 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) = (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) |
503 | 496, 502 | eqtrid 2780 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) = (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) |
504 | 492, 503 | eqtrd 2768 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ π½) = (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) |
505 | 504 | oveq2d 7442 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((mulGrpβπ
)
Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ π½)) = ((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) |
506 | 289 | resmptd 6049 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ (πΌ β π½)) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))) |
507 | | fveq2 6902 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβπ) = (πβπ)) |
508 | | fveq2 6902 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΄βπ) = (π΄βπ)) |
509 | 507, 508 | oveq12d 7444 |
. . . . . . . . . . . . 13
β’ (π = π β ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)) = ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) |
510 | 509 | cbvmptv 5265 |
. . . . . . . . . . . 12
β’ (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) |
511 | | simpr 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β π β (πΌ β π½)) |
512 | 511 | fvresd 6922 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β ((π βΎ (πΌ β π½))βπ) = (πβπ)) |
513 | 511 | fvresd 6922 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β ((π΄ βΎ (πΌ β π½))βπ) = (π΄βπ)) |
514 | 512, 513 | oveq12d 7444 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) = ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) |
515 | 514 | eqcomd 2734 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)) = (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) |
516 | 515 | mpteq2dva 5252 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) = (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) |
517 | 510, 516 | eqtrid 2780 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) = (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) |
518 | 506, 517 | eqtrd 2768 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ (πΌ β π½)) = (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) |
519 | 518 | oveq2d 7442 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((mulGrpβπ
)
Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ (πΌ β π½))) = ((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) |
520 | 505, 519 | oveq12d 7444 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(((mulGrpβπ
)
Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ π½))(.rβπ
)((mulGrpβπ
) Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ (πΌ β π½)))) = (((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
521 | 491, 520 | eqtr2d 2769 |
. . . . . . 7
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(((mulGrpβπ
)
Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = ((mulGrpβπ
) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))))) |
522 | 351, 521 | oveq12d 7444 |
. . . . . 6
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)(((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) = ((πΉβπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))))) |
523 | 473, 522 | eqtrd 2768 |
. . . . 5
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = ((πΉβπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))))) |
524 | 523 | mpteq2dva 5252 |
. . . 4
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) = (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ ((πΉβπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))))))) |
525 | 524 | oveq2d 7442 |
. . 3
β’ (π β (π
Ξ£g (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))) = (π
Ξ£g (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ ((πΉβπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))))))) |
526 | 275, 472,
525 | 3eqtr2d 2774 |
. 2
β’ (π β (π
Ξ£g (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β¦
(((((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½)))βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))) = (π
Ξ£g (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ ((πΉβπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))))))) |
527 | | eqid 2728 |
. . 3
β’ ((πΌ β π½) eval π
) = ((πΌ β π½) eval π
) |
528 | 527, 3, 1, 137, 28, 47, 49, 136, 6, 7, 166, 457 | evlvvval 41837 |
. 2
β’ (π β ((((πΌ β π½) eval π
)β(((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½))))β(π΄ βΎ (πΌ β π½))) = (π
Ξ£g (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β¦
(((((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½)))βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))))) |
529 | | eqid 2728 |
. . 3
β’ (πΌ eval π
) = (πΌ eval π
) |
530 | 529, 14, 15, 282, 28, 47, 49, 136, 4, 7, 17, 35 | evlvvval 41837 |
. 2
β’ (π β (((πΌ eval π
)βπΉ)βπ΄) = (π
Ξ£g (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ ((πΉβπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))))))) |
531 | 526, 528,
530 | 3eqtr4d 2778 |
1
β’ (π β ((((πΌ β π½) eval π
)β(((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½))))β(π΄ βΎ (πΌ β π½))) = (((πΌ eval π
)βπΉ)βπ΄)) |