Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
2 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(.rβπ) = (.rβπ) |
3 | | evlselv.u |
. . . . . . . . . . . . . . . 16
β’ π = ((πΌ β π½) mPoly π
) |
4 | | evlselv.i |
. . . . . . . . . . . . . . . . 17
β’ (π β πΌ β π) |
5 | | difssd 4131 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΌ β π½) β πΌ) |
6 | 4, 5 | ssexd 5323 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΌ β π½) β V) |
7 | | evlselv.r |
. . . . . . . . . . . . . . . 16
β’ (π β π
β CRing) |
8 | 3, 6, 7 | mplcrngd 41115 |
. . . . . . . . . . . . . . 15
β’ (π β π β CRing) |
9 | 8 | crngringd 20062 |
. . . . . . . . . . . . . 14
β’ (π β π β Ring) |
10 | 9 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π β Ring) |
11 | | evlselv.t |
. . . . . . . . . . . . . . . 16
β’ π = (π½ mPoly π) |
12 | | eqid 2732 |
. . . . . . . . . . . . . . . 16
β’
(Baseβπ) =
(Baseβπ) |
13 | | eqid 2732 |
. . . . . . . . . . . . . . . 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 41152 |
. . . . . . . . . . . . . . . 16
β’ (π β (((πΌ selectVars π
)βπ½)βπΉ) β (Baseβπ)) |
19 | 11, 1, 12, 13, 18 | mplelf 21548 |
. . . . . . . . . . . . . . 15
β’ (π β (((πΌ selectVars π
)βπ½)βπΉ):{π β (β0
βm π½)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ)) |
20 | 19 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(((πΌ selectVars π
)βπ½)βπΉ):{π β (β0
βm π½)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ)) |
21 | 20 | ffvelcdmda 7083 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ)βπ) β (Baseβπ)) |
22 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’
(mulGrpβπ) =
(mulGrpβπ) |
23 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’
(.gβ(mulGrpβπ)) =
(.gβ(mulGrpβπ)) |
24 | 4, 16 | ssexd 5323 |
. . . . . . . . . . . . . . 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 6903 |
. . . . . . . . . . . . . . . . 17
β’ (π β (Baseβπ) β V) |
28 | | evlselv.k |
. . . . . . . . . . . . . . . . . . 19
β’ πΎ = (Baseβπ
) |
29 | 28 | fvexi 6902 |
. . . . . . . . . . . . . . . . . 18
β’ πΎ β V |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΎ β V) |
31 | | evlselv.l |
. . . . . . . . . . . . . . . . . 18
β’ πΏ = (algScβπ) |
32 | 7 | crngringd 20062 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π
β Ring) |
33 | 3, 1, 28, 31, 6, 32 | mplasclf 21617 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΏ:πΎβΆ(Baseβπ)) |
34 | 27, 30, 33 | elmapdd 8831 |
. . . . . . . . . . . . . . . 16
β’ (π β πΏ β ((Baseβπ) βm πΎ)) |
35 | | evlselv.a |
. . . . . . . . . . . . . . . . 17
β’ (π β π΄ β (πΎ βm πΌ)) |
36 | 35, 16 | elmapssresd 41063 |
. . . . . . . . . . . . . . . 16
β’ (π β (π΄ βΎ π½) β (πΎ βm π½)) |
37 | 34, 36 | mapcod 41064 |
. . . . . . . . . . . . . . 15
β’ (π β (πΏ β (π΄ βΎ π½)) β ((Baseβπ) βm π½)) |
38 | 37 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (πΏ β (π΄ βΎ π½)) β ((Baseβπ) βm π½)) |
39 | | simpr 485 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π β {π β (β0
βm π½)
β£ (β‘π β β) β
Fin}) |
40 | 13, 1, 22, 23, 25, 26, 38, 39 | evlsvvvallem 41130 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβπ)
Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))) β (Baseβπ)) |
41 | 1, 2, 10, 21, 40 | ringcld 20073 |
. . . . . . . . . . . 12
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))) β (Baseβπ)) |
42 | | eqidd 2733 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))) = (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))) |
43 | | eqidd 2733 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π’ β (Baseβπ) β¦ (π’βπ)) = (π’ β (Baseβπ) β¦ (π’βπ))) |
44 | | fveq1 6887 |
. . . . . . . . . . . 12
β’ (π’ = (((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))) β (π’βπ) = ((((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))βπ)) |
45 | 41, 42, 43, 44 | fmptco 7123 |
. . . . . . . . . . 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 2732 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
48 | 47, 28 | mgpbas 19987 |
. . . . . . . . . . . . . . . . . . . . 21
β’ πΎ =
(Baseβ(mulGrpβπ
)) |
49 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(.gβ(mulGrpβπ
)) =
(.gβ(mulGrpβπ
)) |
50 | 47 | ringmgp 20055 |
. . . . . . . . . . . . . . . . . . . . . . 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 21462 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β π:π½βΆβ0) |
54 | 53 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π:π½βΆβ0) |
55 | 54 | ffvelcdmda 7083 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β (πβπ) β
β0) |
56 | | elmapi 8839 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π΄ β (πΎ βm πΌ) β π΄:πΌβΆπΎ) |
57 | 35, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π΄:πΌβΆπΎ) |
58 | 57, 16 | fssresd 6755 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π΄ βΎ π½):π½βΆπΎ) |
59 | 58 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π΄ βΎ π½):π½βΆπΎ) |
60 | 59 | ffvelcdmda 7083 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β ((π΄ βΎ π½)βπ) β πΎ) |
61 | 48, 49, 52, 55, 60 | mulgnn0cld 18969 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) β πΎ) |
62 | 46, 61 | cofmpt 7126 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (πΏ β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) = (π β π½ β¦ (πΏβ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) |
63 | 3 | mplassa 21572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((πΌ β π½) β V β§ π
β CRing) β π β AssAlg) |
64 | 6, 7, 63 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π β AssAlg) |
65 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(Scalarβπ) =
(Scalarβπ) |
66 | 31, 65 | asclrhm 21435 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β AssAlg β πΏ β ((Scalarβπ) RingHom π)) |
67 | 64, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β πΏ β ((Scalarβπ) RingHom π)) |
68 | 3, 6, 7 | mplsca 21563 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π
= (Scalarβπ)) |
69 | 68 | eqcomd 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (Scalarβπ) = π
) |
70 | 69 | oveq1d 7420 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β ((Scalarβπ) RingHom π) = (π
RingHom π)) |
71 | 67, 70 | eleqtrd 2835 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΏ β (π
RingHom π)) |
72 | 47, 22 | rhmmhm 20250 |
. . . . . . . . . . . . . . . . . . . . . . . 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 18989 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΏ β ((mulGrpβπ
) MndHom (mulGrpβπ)) β§ (πβπ) β β0 β§ ((π΄ βΎ π½)βπ) β πΎ) β (πΏβ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) = ((πβπ)(.gβ(mulGrpβπ))(πΏβ((π΄ βΎ π½)βπ)))) |
76 | 74, 55, 60, 75 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β (πΏβ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) = ((πβπ)(.gβ(mulGrpβπ))(πΏβ((π΄ βΎ π½)βπ)))) |
77 | 58 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β (π΄ βΎ π½):π½βΆπΎ) |
78 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β π β π½) |
79 | 77, 78 | fvco3d 6988 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β ((πΏ β (π΄ βΎ π½))βπ) = (πΏβ((π΄ βΎ π½)βπ))) |
80 | 79 | oveq2d 7421 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)) = ((πβπ)(.gβ(mulGrpβπ))(πΏβ((π΄ βΎ π½)βπ)))) |
81 | 76, 80 | eqtr4d 2775 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β (πΏβ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) = ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))) |
82 | 81 | mpteq2dva 5247 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ (πΏβ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))) |
83 | 62, 82 | eqtrd 2772 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (πΏ β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))) |
84 | 83 | oveq2d 7421 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβπ)
Ξ£g (πΏ β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) = ((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))) |
85 | | eqid 2732 |
. . . . . . . . . . . . . . . . . 18
β’
(Baseβ(mulGrpβ(Scalarβπ))) =
(Baseβ(mulGrpβ(Scalarβπ))) |
86 | | eqid 2732 |
. . . . . . . . . . . . . . . . . 18
β’
(0gβ(mulGrpβ(Scalarβπ))) =
(0gβ(mulGrpβ(Scalarβπ))) |
87 | 68, 7 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (Scalarβπ) β CRing) |
88 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(mulGrpβ(Scalarβπ)) = (mulGrpβ(Scalarβπ)) |
89 | 88 | crngmgp 20057 |
. . . . . . . . . . . . . . . . . . . 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 20055 |
. . . . . . . . . . . . . . . . . . . 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 20250 |
. . . . . . . . . . . . . . . . . . . 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 6892 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (Baseβπ
) =
(Baseβ(Scalarβπ))) |
99 | 28, 98 | eqtrid 2784 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β πΎ = (Baseβ(Scalarβπ))) |
100 | 99 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β πΎ = (Baseβ(Scalarβπ))) |
101 | 61, 100 | eleqtrd 2835 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) β (Baseβ(Scalarβπ))) |
102 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
103 | 88, 102 | mgpbas 19987 |
. . . . . . . . . . . . . . . . . . . 20
β’
(Baseβ(Scalarβπ)) =
(Baseβ(mulGrpβ(Scalarβπ))) |
104 | 101, 103 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β π½) β ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) β
(Baseβ(mulGrpβ(Scalarβπ)))) |
105 | 104 | fmpttd 7111 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))):π½βΆ(Baseβ(mulGrpβ(Scalarβπ)))) |
106 | 24 | mptexd 7222 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) β V) |
107 | 106 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) β V) |
108 | | fvexd 6903 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(0gβ(mulGrpβπ
)) β V) |
109 | | funmpt 6583 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ Fun
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) |
110 | 109 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β Fun
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) |
111 | 54 | feqmptd 6957 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π = (π β π½ β¦ (πβπ))) |
112 | 13 | psrbagfsupp 21464 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β π finSupp 0) |
113 | 112 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π finSupp 0) |
114 | 111, 113 | eqbrtrrd 5171 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ (πβπ)) finSupp 0) |
115 | | ssidd 4004 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β ((π β π½ β¦ (πβπ)) supp 0) β ((π β π½ β¦ (πβπ)) supp 0)) |
116 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(0gβ(mulGrpβπ
)) =
(0gβ(mulGrpβπ
)) |
117 | 48, 116, 49 | mulg0 18951 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β πΎ β
(0(.gβ(mulGrpβπ
))π) = (0gβ(mulGrpβπ
))) |
118 | 117 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β πΎ) β
(0(.gβ(mulGrpβπ
))π) = (0gβ(mulGrpβπ
))) |
119 | | 0zd 12566 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β 0
β β€) |
120 | 115, 118,
55, 60, 119 | suppssov1 8179 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β ((π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) supp
(0gβ(mulGrpβπ
))) β ((π β π½ β¦ (πβπ)) supp 0)) |
121 | 107, 108,
110, 114, 120 | fsuppsssuppgd 41061 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) finSupp
(0gβ(mulGrpβπ
))) |
122 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(1rβπ
) = (1rβπ
) |
123 | 47, 122 | ringidval 20000 |
. . . . . . . . . . . . . . . . . . . 20
β’
(1rβπ
) = (0gβ(mulGrpβπ
)) |
124 | 121, 123 | breqtrrdi 5189 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) finSupp (1rβπ
)) |
125 | 68 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1rβπ
) =
(1rβ(Scalarβπ))) |
126 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
127 | 88, 126 | ringidval 20000 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(1rβ(Scalarβπ)) =
(0gβ(mulGrpβ(Scalarβπ))) |
128 | 125, 127 | eqtrdi 2788 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1rβπ
) =
(0gβ(mulGrpβ(Scalarβπ)))) |
129 | 128 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(1rβπ
) =
(0gβ(mulGrpβ(Scalarβπ)))) |
130 | 124, 129 | breqtrd 5173 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) finSupp
(0gβ(mulGrpβ(Scalarβπ)))) |
131 | 85, 86, 91, 94, 25, 97, 105, 130 | gsummhm 19800 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβπ)
Ξ£g (πΏ β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) = (πΏβ((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
132 | 84, 131 | eqtr3d 2774 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβπ)
Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))) = (πΏβ((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
133 | 132 | oveq2d 7421 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))) = (((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)(πΏβ((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))))) |
134 | 64 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π β AssAlg) |
135 | 101 | fmpttd 7111 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))):π½βΆ(Baseβ(Scalarβπ))) |
136 | 130, 127 | breqtrrdi 5189 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) finSupp
(1rβ(Scalarβπ))) |
137 | 103, 127,
91, 25, 135, 136 | gsumcl 19777 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) β (Baseβ(Scalarβπ))) |
138 | | eqid 2732 |
. . . . . . . . . . . . . . . . 17
β’ (
Β·π βπ) = ( Β·π
βπ) |
139 | 31, 65, 102, 1, 2, 138 | asclmul2 21432 |
. . . . . . . . . . . . . . . 16
β’ ((π β AssAlg β§
((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) β (Baseβ(Scalarβπ)) β§ ((((πΌ selectVars π
)βπ½)βπΉ)βπ) β (Baseβπ)) β (((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)(πΏβ((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) = (((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))( Β·π
βπ)((((πΌ selectVars π
)βπ½)βπΉ)βπ))) |
140 | 134, 137,
21, 139 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)(πΏβ((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) = (((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))( Β·π
βπ)((((πΌ selectVars π
)βπ½)βπΉ)βπ))) |
141 | 133, 140 | eqtrd 2772 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))) = (((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))( Β·π
βπ)((((πΌ selectVars π
)βπ½)βπΉ)βπ))) |
142 | 141 | fveq1d 6890 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))βπ) = ((((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))( Β·π
βπ)((((πΌ selectVars π
)βπ½)βπΉ)βπ))βπ)) |
143 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’
(.rβπ
) = (.rβπ
) |
144 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’ {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} = {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β
Fin} |
145 | 99 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β πΎ =
(Baseβ(Scalarβπ))) |
146 | 137, 145 | eleqtrrd 2836 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) β πΎ) |
147 | | simplr 767 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β
Fin}) |
148 | 3, 138, 28, 1, 143, 144, 146, 21, 147 | mplvscaval 21566 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))( Β·π
βπ)((((πΌ selectVars π
)βπ½)βπΉ)βπ))βπ) = (((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ))) |
149 | 142, 148 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))βπ) = (((mulGrpβ(Scalarβπ)) Ξ£g
(π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ))) |
150 | 149 | mpteq2dva 5247 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))βπ)) = (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)))) |
151 | 45, 150 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β ((π’ β (Baseβπ) β¦ (π’βπ)) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))) = (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)))) |
152 | 151 | oveq2d 7421 |
. . . . . . . . 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 π
)βπ½)βπΉ)βπ)βπ))))) |
153 | 69 | fveq2d 6892 |
. . . . . . . . . . . . . . 15
β’ (π β
(mulGrpβ(Scalarβπ)) = (mulGrpβπ
)) |
154 | 153 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(mulGrpβ(Scalarβπ)) = (mulGrpβπ
)) |
155 | 154 | oveq1d 7420 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) = ((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) |
156 | 155 | oveq1d 7420 |
. . . . . . . . . . . 12
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) = (((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ))) |
157 | 7 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π
β CRing) |
158 | 155, 146 | eqeltrrd 2834 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((mulGrpβπ
)
Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) β πΎ) |
159 | 19 | ffvelcdmda 7083 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ)βπ) β (Baseβπ)) |
160 | 3, 28, 1, 144, 159 | mplelf 21548 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ)βπ):{π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}βΆπΎ) |
161 | 160 | ffvelcdmda 7083 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) β πΎ) |
162 | 161 | an32s 650 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) β πΎ) |
163 | 28, 143, 157, 158, 162 | crngcomd 41084 |
. . . . . . . . . . . 12
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((mulGrpβπ
)
Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) = ((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
164 | 156, 163 | eqtrd 2772 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) = ((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
165 | 164 | mpteq2dva 5247 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((mulGrpβ(Scalarβπ)) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ))) = (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))))) |
166 | 165 | oveq2d 7421 |
. . . . . . . . 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βπ
))((π΄ βΎ π½)βπ)))))))) |
167 | 152, 166 | eqtrd 2772 |
. . . . . . . 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βπ
))((π΄ βΎ π½)βπ)))))))) |
168 | 167 | oveq1d 7420 |
. . . . . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
169 | | eqid 2732 |
. . . . . . . . . 10
β’ (π’ β (Baseβπ) β¦ (π’βπ)) = (π’ β (Baseβπ) β¦ (π’βπ)) |
170 | | fveq1 6887 |
. . . . . . . . . 10
β’ (π’ = (π Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))) β (π’βπ) = ((π Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))))βπ)) |
171 | | eqid 2732 |
. . . . . . . . . . . . 13
β’ (π½ eval π) = (π½ eval π) |
172 | 171, 11, 12, 13, 1, 22, 23, 2, 24, 8, 18, 37 | evlvvval 41142 |
. . . . . . . . . . . 12
β’ (π β (((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½))) = (π Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))))) |
173 | 171, 11, 12, 1, 24, 8, 18, 37 | evlcl 41141 |
. . . . . . . . . . . 12
β’ (π β (((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½))) β (Baseβπ)) |
174 | 172, 173 | eqeltrrd 2834 |
. . . . . . . . . . 11
β’ (π β (π Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))) β (Baseβπ)) |
175 | 174 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π Ξ£g
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))) β (Baseβπ)) |
176 | | fvexd 6903 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β ((π Ξ£g
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))))βπ) β V) |
177 | 169, 170,
175, 176 | fvmptd3 7018 |
. . . . . . . . 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βπ))((πΏ β (π΄ βΎ π½))βπ)))))))βπ)) |
178 | | eqid 2732 |
. . . . . . . . . 10
β’
(0gβπ) = (0gβπ) |
179 | 9 | ringcmnd 20094 |
. . . . . . . . . . 11
β’ (π β π β CMnd) |
180 | 179 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π β CMnd) |
181 | 7 | crnggrpd 20063 |
. . . . . . . . . . . 12
β’ (π β π
β Grp) |
182 | 181 | grpmndd 18828 |
. . . . . . . . . . 11
β’ (π β π
β Mnd) |
183 | 182 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π
β Mnd) |
184 | | ovex 7438 |
. . . . . . . . . . . 12
β’
(β0 βm π½) β V |
185 | 184 | rabex 5331 |
. . . . . . . . . . 11
β’ {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β
V |
186 | 185 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β
V) |
187 | 6 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (πΌ β π½) β V) |
188 | 181 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π
β Grp) |
189 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β
Fin}) |
190 | 3, 1, 144, 169, 187, 188, 189 | mplmapghm 41125 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π’ β (Baseβπ) β¦ (π’βπ)) β (π GrpHom π
)) |
191 | | ghmmhm 19096 |
. . . . . . . . . . 11
β’ ((π’ β (Baseβπ) β¦ (π’βπ)) β (π GrpHom π
) β (π’ β (Baseβπ) β¦ (π’βπ)) β (π MndHom π
)) |
192 | 190, 191 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π’ β (Baseβπ) β¦ (π’βπ)) β (π MndHom π
)) |
193 | 41 | fmpttd 7111 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))):{π β (β0
βm π½)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ)) |
194 | 24 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π½ β V) |
195 | 8 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π β CRing) |
196 | 18 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(((πΌ selectVars π
)βπ½)βπΉ) β (Baseβπ)) |
197 | 37 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (πΏ β (π΄ βΎ π½)) β ((Baseβπ) βm π½)) |
198 | 13, 11, 12, 1, 22, 23, 2, 194, 195, 196, 197 | evlvvvallem 41143 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))) finSupp (0gβπ)) |
199 | 1, 178, 180, 183, 186, 192, 193, 198 | gsummhm 19800 |
. . . . . . . . 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βπ))((πΏ β (π΄ βΎ π½))βπ))))))))) |
200 | 172 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½))) = (π Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))))) |
201 | 200 | fveq1d 6890 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
((((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½)))βπ) = ((π Ξ£g (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ)))))))βπ)) |
202 | 177, 199,
201 | 3eqtr4rd 2783 |
. . . . . . . 8
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
((((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½)))βπ) = (π
Ξ£g ((π’ β (Baseβπ) β¦ (π’βπ)) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)(.rβπ)((mulGrpβπ) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ))((πΏ β (π΄ βΎ π½))βπ))))))))) |
203 | 202 | oveq1d 7420 |
. . . . . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
204 | | eqid 2732 |
. . . . . . . 8
β’
(0gβπ
) = (0gβπ
) |
205 | 32 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π
β Ring) |
206 | 47 | crngmgp 20057 |
. . . . . . . . . . 11
β’ (π
β CRing β
(mulGrpβπ
) β
CMnd) |
207 | 7, 206 | syl 17 |
. . . . . . . . . 10
β’ (π β (mulGrpβπ
) β CMnd) |
208 | 207 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(mulGrpβπ
) β
CMnd) |
209 | 51 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β (πΌ β π½)) β (mulGrpβπ
) β Mnd) |
210 | 144 | psrbagf 21462 |
. . . . . . . . . . . . 13
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β π:(πΌ β π½)βΆβ0) |
211 | 210 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π:(πΌ β π½)βΆβ0) |
212 | 211 | ffvelcdmda 7083 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β (πΌ β π½)) β (πβπ) β
β0) |
213 | 57, 5 | fssresd 6755 |
. . . . . . . . . . . . 13
β’ (π β (π΄ βΎ (πΌ β π½)):(πΌ β π½)βΆπΎ) |
214 | 213 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π΄ βΎ (πΌ β π½)):(πΌ β π½)βΆπΎ) |
215 | 214 | ffvelcdmda 7083 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β (πΌ β π½)) β ((π΄ βΎ (πΌ β π½))βπ) β πΎ) |
216 | 48, 49, 209, 212, 215 | mulgnn0cld 18969 |
. . . . . . . . . 10
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β (πΌ β π½)) β ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) β πΎ) |
217 | 216 | fmpttd 7111 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))):(πΌ β π½)βΆπΎ) |
218 | 6 | mptexd 7222 |
. . . . . . . . . . 11
β’ (π β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) β V) |
219 | 218 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) β V) |
220 | | fvexd 6903 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(0gβ(mulGrpβπ
)) β V) |
221 | | funmpt 6583 |
. . . . . . . . . . 11
β’ Fun
(π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) |
222 | 221 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β Fun
(π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) |
223 | 211 | feqmptd 6957 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π = (π β (πΌ β π½) β¦ (πβπ))) |
224 | 144 | psrbagfsupp 21464 |
. . . . . . . . . . . 12
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β π finSupp 0) |
225 | 224 | adantl 482 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β π finSupp 0) |
226 | 223, 225 | eqbrtrrd 5171 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β (πΌ β π½) β¦ (πβπ)) finSupp 0) |
227 | | ssidd 4004 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β ((π β (πΌ β π½) β¦ (πβπ)) supp 0) β ((π β (πΌ β π½) β¦ (πβπ)) supp 0)) |
228 | 48, 116, 49 | mulg0 18951 |
. . . . . . . . . . . 12
β’ (π£ β πΎ β
(0(.gβ(mulGrpβπ
))π£) = (0gβ(mulGrpβπ
))) |
229 | 228 | adantl 482 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π£ β πΎ) β
(0(.gβ(mulGrpβπ
))π£) = (0gβ(mulGrpβπ
))) |
230 | | fvexd 6903 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β (πΌ β π½)) β (πβπ) β V) |
231 | | 0zd 12566 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β 0
β β€) |
232 | 227, 229,
230, 215, 231 | suppssov1 8179 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β ((π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) supp
(0gβ(mulGrpβπ
))) β ((π β (πΌ β π½) β¦ (πβπ)) supp 0)) |
233 | 219, 220,
222, 226, 232 | fsuppsssuppgd 41061 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) finSupp
(0gβ(mulGrpβπ
))) |
234 | 48, 116, 208, 187, 217, 233 | gsumcl 19777 |
. . . . . . . 8
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
((mulGrpβπ
)
Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) β πΎ) |
235 | 32 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β π
β Ring) |
236 | 28, 143, 235, 162, 158 | ringcld 20073 |
. . . . . . . 8
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) β πΎ) |
237 | 185 | mptex 7221 |
. . . . . . . . . 10
β’ (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) β V |
238 | 237 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) β V) |
239 | | fvexd 6903 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(0gβπ
)
β V) |
240 | | funmpt 6583 |
. . . . . . . . . 10
β’ Fun
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
241 | 240 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β Fun
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))))) |
242 | 185 | mptex 7221 |
. . . . . . . . . . 11
β’ (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) β V |
243 | 242 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) β V) |
244 | | funmpt 6583 |
. . . . . . . . . . 11
β’ Fun
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) |
245 | 244 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β Fun
(π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ))) |
246 | 11, 12, 178, 18, 8 | mplelsfi 21545 |
. . . . . . . . . . 11
β’ (π β (((πΌ selectVars π
)βπ½)βπΉ) finSupp (0gβπ)) |
247 | 246 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(((πΌ selectVars π
)βπ½)βπΉ) finSupp (0gβπ)) |
248 | | ssidd 4004 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ) supp (0gβπ)) β ((((πΌ selectVars π
)βπ½)βπΉ) supp (0gβπ))) |
249 | | fvexd 6903 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(0gβπ)
β V) |
250 | 20, 248, 186, 249 | suppssr 8177 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β ({π β (β0
βm π½)
β£ (β‘π β β) β Fin} β
((((πΌ selectVars π
)βπ½)βπΉ) supp (0gβπ)))) β ((((πΌ selectVars π
)βπ½)βπΉ)βπ) = (0gβπ)) |
251 | 250 | fveq1d 6890 |
. . . . . . . . . . . 12
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β ({π β (β0
βm π½)
β£ (β‘π β β) β Fin} β
((((πΌ selectVars π
)βπ½)βπΉ) supp (0gβπ)))) β (((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) = ((0gβπ)βπ)) |
252 | 3, 144, 204, 178, 6, 181 | mpl0 21556 |
. . . . . . . . . . . . . . . 16
β’ (π β (0gβπ) = ({π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} Γ
{(0gβπ
)})) |
253 | 252 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(0gβπ) =
({π β
(β0 βm (πΌ β π½)) β£ (β‘π β β) β Fin} Γ
{(0gβπ
)})) |
254 | 253 | fveq1d 6890 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
((0gβπ)βπ) = (({π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} Γ
{(0gβπ
)})βπ)) |
255 | | fvex 6901 |
. . . . . . . . . . . . . . . 16
β’
(0gβπ
) β V |
256 | 255 | fvconst2 7201 |
. . . . . . . . . . . . . . 15
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β (({π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} Γ
{(0gβπ
)})βπ) = (0gβπ
)) |
257 | 256 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(({π β
(β0 βm (πΌ β π½)) β£ (β‘π β β) β Fin} Γ
{(0gβπ
)})βπ) = (0gβπ
)) |
258 | 254, 257 | eqtrd 2772 |
. . . . . . . . . . . . 13
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
((0gβπ)βπ) = (0gβπ
)) |
259 | 258 | adantr 481 |
. . . . . . . . . . . 12
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β ({π β (β0
βm π½)
β£ (β‘π β β) β Fin} β
((((πΌ selectVars π
)βπ½)βπΉ) supp (0gβπ)))) β
((0gβπ)βπ) = (0gβπ
)) |
260 | 251, 259 | eqtrd 2772 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β ({π β (β0
βm π½)
β£ (β‘π β β) β Fin} β
((((πΌ selectVars π
)βπ½)βπΉ) supp (0gβπ)))) β (((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) = (0gβπ
)) |
261 | 260, 186 | suppss2 8181 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β ((π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) supp (0gβπ
)) β ((((πΌ selectVars π
)βπ½)βπΉ) supp (0gβπ))) |
262 | 243, 239,
245, 247, 261 | fsuppsssuppgd 41061 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) finSupp (0gβπ
)) |
263 | | ssidd 4004 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β ((π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) supp (0gβπ
)) β ((π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) supp (0gβπ
))) |
264 | 32 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π£ β πΎ) β π
β Ring) |
265 | | simpr 485 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π£ β πΎ) β π£ β πΎ) |
266 | 28, 143, 204, 264, 265 | ringlzd 41082 |
. . . . . . . . . 10
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π£ β πΎ) β ((0gβπ
)(.rβπ
)π£) = (0gβπ
)) |
267 | 263, 266,
162, 158, 239 | suppssov1 8179 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β ((π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) supp (0gβπ
)) β ((π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) supp (0gβπ
))) |
268 | 238, 239,
241, 262, 267 | fsuppsssuppgd 41061 |
. . . . . . . 8
β’ ((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) finSupp (0gβπ
)) |
269 | 28, 204, 143, 205, 186, 234, 236, 268 | gsummulc1 20121 |
. . . . . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
270 | 168, 203,
269 | 3eqtr4d 2782 |
. . . . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ)))))))) |
271 | | fveq2 6888 |
. . . . . . . . . . . . . 14
β’ (π = π β ((((πΌ selectVars π
)βπ½)βπΉ)βπ) = ((((πΌ selectVars π
)βπ½)βπΉ)βπ)) |
272 | 271 | adantl 482 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = π) β ((((πΌ selectVars π
)βπ½)βπΉ)βπ) = ((((πΌ selectVars π
)βπ½)βπΉ)βπ)) |
273 | | simpl 483 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = π) β π = π) |
274 | 272, 273 | fveq12d 6895 |
. . . . . . . . . . . 12
β’ ((π = π β§ π = π) β (((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) = (((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) |
275 | | fveq1 6887 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πβπ) = (πβπ)) |
276 | 275 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ ((π = π β§ π = π) β (πβπ) = (πβπ)) |
277 | 276 | oveq1d 7420 |
. . . . . . . . . . . . . 14
β’ ((π = π β§ π = π) β ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) |
278 | 277 | mpteq2dv 5249 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = π) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) |
279 | 278 | oveq2d 7421 |
. . . . . . . . . . . 12
β’ ((π = π β§ π = π) β ((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) = ((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) |
280 | 274, 279 | oveq12d 7423 |
. . . . . . . . . . 11
β’ ((π = π β§ π = π) β ((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) = ((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
281 | | fveq1 6887 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβπ) = (πβπ)) |
282 | 281 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π = π β§ π = π) β (πβπ) = (πβπ)) |
283 | 282 | oveq1d 7420 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = π) β ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) = ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) |
284 | 283 | mpteq2dv 5249 |
. . . . . . . . . . . 12
β’ ((π = π β§ π = π) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) |
285 | 284 | oveq2d 7421 |
. . . . . . . . . . 11
β’ ((π = π β§ π = π) β ((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) = ((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) |
286 | 280, 285 | oveq12d 7423 |
. . . . . . . . . 10
β’ ((π = π β§ π = π) β (((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = (((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
287 | | eqid 2732 |
. . . . . . . . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
288 | | ovex 7438 |
. . . . . . . . . 10
β’
(((((((πΌ selectVars
π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) β V |
289 | 286, 287,
288 | ovmpoa 7559 |
. . . . . . . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
290 | 289 | 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βπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
291 | 290 | mpteq2dva 5247 |
. . . . . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ))))))) |
292 | 291 | oveq2d 7421 |
. . . . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ)))))))) |
293 | 270, 292 | eqtr4d 2775 |
. . . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ))))))π)))) |
294 | 293 | mpteq2dva 5247 |
. . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ))))))π))))) |
295 | 294 | oveq2d 7421 |
. . 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βπ
))((π΄ βΎ (πΌ β π½))βπ))))))π)))))) |
296 | 32 | ringcmnd 20094 |
. . . . 5
β’ (π β π
β CMnd) |
297 | | ovex 7438 |
. . . . . . 7
β’
(β0 βm πΌ) β V |
298 | 297 | rabex 5331 |
. . . . . 6
β’ {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β
V |
299 | 298 | a1i 11 |
. . . . 5
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β
V) |
300 | 32 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π
β Ring) |
301 | 19 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (((πΌ selectVars π
)βπ½)βπΉ):{π β (β0
βm π½)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ)) |
302 | | eqid 2732 |
. . . . . . . . . . . 12
β’ {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} = {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
303 | 4 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β πΌ β π) |
304 | 16 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π½ β πΌ) |
305 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π β {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
306 | 302, 13, 303, 304, 305 | psrbagres 41112 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βΎ π½) β {π β (β0
βm π½)
β£ (β‘π β β) β
Fin}) |
307 | 301, 306 | ffvelcdmd 7084 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½)) β (Baseβπ)) |
308 | 3, 28, 1, 144, 307 | mplelf 21548 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½)):{π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}βΆπΎ) |
309 | | difssd 4131 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (πΌ β π½) β πΌ) |
310 | 302, 144,
303, 309, 305 | psrbagres 41112 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βΎ (πΌ β π½)) β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β
Fin}) |
311 | 308, 310 | ffvelcdmd 7084 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½))) β πΎ) |
312 | 207 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(mulGrpβπ
) β
CMnd) |
313 | 24 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π½ β V) |
314 | 51 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β (mulGrpβπ
) β Mnd) |
315 | 302 | psrbagf 21462 |
. . . . . . . . . . . . . 14
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β π:πΌβΆβ0) |
316 | 315 | adantl 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π:πΌβΆβ0) |
317 | 316, 304 | fssresd 6755 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βΎ π½):π½βΆβ0) |
318 | 317 | ffvelcdmda 7083 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β ((π βΎ π½)βπ) β
β0) |
319 | 58 | ffvelcdmda 7083 |
. . . . . . . . . . . 12
β’ ((π β§ π β π½) β ((π΄ βΎ π½)βπ) β πΎ) |
320 | 319 | adantlr 713 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β ((π΄ βΎ π½)βπ) β πΎ) |
321 | 48, 49, 314, 318, 320 | mulgnn0cld 18969 |
. . . . . . . . . 10
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) β πΎ) |
322 | 321 | fmpttd 7111 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))):π½βΆπΎ) |
323 | 24 | mptexd 7222 |
. . . . . . . . . . 11
β’ (π β (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) β V) |
324 | 323 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) β V) |
325 | | fvexd 6903 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(0gβ(mulGrpβπ
)) β V) |
326 | | funmpt 6583 |
. . . . . . . . . . 11
β’ Fun
(π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) |
327 | 326 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β Fun
(π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) |
328 | 302 | psrbagfsupp 21464 |
. . . . . . . . . . . 12
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β π finSupp 0) |
329 | 328 | adantl 482 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π finSupp 0) |
330 | | 0zd 12566 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β 0 β
β€) |
331 | 329, 330 | fsuppres 9384 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βΎ π½) finSupp 0) |
332 | | ssidd 4004 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π βΎ π½) supp 0) β ((π βΎ π½) supp 0)) |
333 | 317, 332,
313, 330 | suppssr 8177 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (π½ β ((π βΎ π½) supp 0))) β ((π βΎ π½)βπ) = 0) |
334 | 333 | oveq1d 7420 |
. . . . . . . . . . . 12
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (π½ β ((π βΎ π½) supp 0))) β (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) =
(0(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) |
335 | | eldifi 4125 |
. . . . . . . . . . . . 13
β’ (π β (π½ β ((π βΎ π½) supp 0)) β π β π½) |
336 | 48, 116, 49 | mulg0 18951 |
. . . . . . . . . . . . . 14
β’ (((π΄ βΎ π½)βπ) β πΎ β
(0(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = (0gβ(mulGrpβπ
))) |
337 | 320, 336 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β
(0(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = (0gβ(mulGrpβπ
))) |
338 | 335, 337 | sylan2 593 |
. . . . . . . . . . . 12
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (π½ β ((π βΎ π½) supp 0))) β
(0(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = (0gβ(mulGrpβπ
))) |
339 | 334, 338 | eqtrd 2772 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (π½ β ((π βΎ π½) supp 0))) β (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = (0gβ(mulGrpβπ
))) |
340 | 339, 313 | suppss2 8181 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) supp
(0gβ(mulGrpβπ
))) β ((π βΎ π½) supp 0)) |
341 | 324, 325,
327, 331, 340 | fsuppsssuppgd 41061 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) finSupp
(0gβ(mulGrpβπ
))) |
342 | 48, 116, 312, 313, 322, 341 | gsumcl 19777 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((mulGrpβπ
)
Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) β πΎ) |
343 | 28, 143, 300, 311, 342 | ringcld 20073 |
. . . . . . 7
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) β πΎ) |
344 | 6 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (πΌ β π½) β V) |
345 | 51 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β (mulGrpβπ
) β Mnd) |
346 | 316, 309 | fssresd 6755 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βΎ (πΌ β π½)):(πΌ β π½)βΆβ0) |
347 | 346 | ffvelcdmda 7083 |
. . . . . . . . . 10
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β ((π βΎ (πΌ β π½))βπ) β
β0) |
348 | 213 | ffvelcdmda 7083 |
. . . . . . . . . . 11
β’ ((π β§ π β (πΌ β π½)) β ((π΄ βΎ (πΌ β π½))βπ) β πΎ) |
349 | 348 | adantlr 713 |
. . . . . . . . . 10
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β ((π΄ βΎ (πΌ β π½))βπ) β πΎ) |
350 | 48, 49, 345, 347, 349 | mulgnn0cld 18969 |
. . . . . . . . 9
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) β πΎ) |
351 | 350 | fmpttd 7111 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))):(πΌ β π½)βΆπΎ) |
352 | 344 | mptexd 7222 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) β V) |
353 | | funmpt 6583 |
. . . . . . . . . 10
β’ Fun
(π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) |
354 | 353 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β Fun
(π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) |
355 | 329, 330 | fsuppres 9384 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βΎ (πΌ β π½)) finSupp 0) |
356 | | ssidd 4004 |
. . . . . . . . . . . . 13
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π βΎ (πΌ β π½)) supp 0) β ((π βΎ (πΌ β π½)) supp 0)) |
357 | 346, 356,
344, 330 | suppssr 8177 |
. . . . . . . . . . . 12
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β ((πΌ β π½) β ((π βΎ (πΌ β π½)) supp 0))) β ((π βΎ (πΌ β π½))βπ) = 0) |
358 | 357 | oveq1d 7420 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β ((πΌ β π½) β ((π βΎ (πΌ β π½)) supp 0))) β (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) =
(0(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) |
359 | | eldifi 4125 |
. . . . . . . . . . . . 13
β’ (π β ((πΌ β π½) β ((π βΎ (πΌ β π½)) supp 0)) β π β (πΌ β π½)) |
360 | 359, 349 | sylan2 593 |
. . . . . . . . . . . 12
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β ((πΌ β π½) β ((π βΎ (πΌ β π½)) supp 0))) β ((π΄ βΎ (πΌ β π½))βπ) β πΎ) |
361 | 48, 116, 49 | mulg0 18951 |
. . . . . . . . . . . 12
β’ (((π΄ βΎ (πΌ β π½))βπ) β πΎ β
(0(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) = (0gβ(mulGrpβπ
))) |
362 | 360, 361 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β ((πΌ β π½) β ((π βΎ (πΌ β π½)) supp 0))) β
(0(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) = (0gβ(mulGrpβπ
))) |
363 | 358, 362 | eqtrd 2772 |
. . . . . . . . . 10
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β ((πΌ β π½) β ((π βΎ (πΌ β π½)) supp 0))) β (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) = (0gβ(mulGrpβπ
))) |
364 | 363, 344 | suppss2 8181 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) supp
(0gβ(mulGrpβπ
))) β ((π βΎ (πΌ β π½)) supp 0)) |
365 | 352, 325,
354, 355, 364 | fsuppsssuppgd 41061 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) finSupp
(0gβ(mulGrpβπ
))) |
366 | 48, 116, 312, 344, 351, 365 | gsumcl 19777 |
. . . . . . 7
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((mulGrpβπ
)
Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) β πΎ) |
367 | 28, 143, 300, 343, 366 | ringcld 20073 |
. . . . . 6
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) β πΎ) |
368 | 367 | fmpttd 7111 |
. . . . 5
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))):{β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}βΆπΎ) |
369 | 298 | mptex 7221 |
. . . . . . 7
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) β V |
370 | 369 | a1i 11 |
. . . . . 6
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) β V) |
371 | | fvexd 6903 |
. . . . . 6
β’ (π β (0gβπ
) β V) |
372 | | funmpt 6583 |
. . . . . . 7
β’ Fun
(π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
373 | 372 | a1i 11 |
. . . . . 6
β’ (π β Fun (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))) |
374 | 298 | mptex 7221 |
. . . . . . . 8
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) β V |
375 | 374 | a1i 11 |
. . . . . . 7
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) β V) |
376 | | funmpt 6583 |
. . . . . . . 8
β’ Fun
(π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
377 | 376 | a1i 11 |
. . . . . . 7
β’ (π β Fun (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))))) |
378 | 7 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π
β CRing) |
379 | 17 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β πΉ β π΅) |
380 | 302, 14, 15, 303, 378, 304, 379, 305 | selvvvval 41154 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½))) = (πΉβπ)) |
381 | 380 | mpteq2dva 5247 |
. . . . . . . 8
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))) = (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (πΉβπ))) |
382 | | eqid 2732 |
. . . . . . . . . . 11
β’
(Baseβπ
) =
(Baseβπ
) |
383 | 14, 382, 15, 302, 17 | mplelf 21548 |
. . . . . . . . . 10
β’ (π β πΉ:{β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}βΆ(Baseβπ
)) |
384 | 383 | feqmptd 6957 |
. . . . . . . . 9
β’ (π β πΉ = (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (πΉβπ))) |
385 | 14, 15, 204, 17, 7 | mplelsfi 21545 |
. . . . . . . . 9
β’ (π β πΉ finSupp (0gβπ
)) |
386 | 384, 385 | eqbrtrrd 5171 |
. . . . . . . 8
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (πΉβπ)) finSupp (0gβπ
)) |
387 | 381, 386 | eqbrtrd 5169 |
. . . . . . 7
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))) finSupp (0gβπ
)) |
388 | | ssidd 4004 |
. . . . . . . 8
β’ (π β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))) supp (0gβπ
)) β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))) supp (0gβπ
))) |
389 | 32 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π£ β πΎ) β π
β Ring) |
390 | | simpr 485 |
. . . . . . . . 9
β’ ((π β§ π£ β πΎ) β π£ β πΎ) |
391 | 28, 143, 204, 389, 390 | ringlzd 41082 |
. . . . . . . 8
β’ ((π β§ π£ β πΎ) β ((0gβπ
)(.rβπ
)π£) = (0gβπ
)) |
392 | | fvexd 6903 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½))) β V) |
393 | 388, 391,
392, 342, 371 | suppssov1 8179 |
. . . . . . 7
β’ (π β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) supp (0gβπ
)) β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))) supp (0gβπ
))) |
394 | 375, 371,
377, 387, 393 | fsuppsssuppgd 41061 |
. . . . . 6
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) finSupp (0gβπ
)) |
395 | | ssidd 4004 |
. . . . . . 7
β’ (π β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) supp (0gβπ
)) β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) supp (0gβπ
))) |
396 | | ovexd 7440 |
. . . . . . 7
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) β V) |
397 | 395, 391,
396, 366, 371 | suppssov1 8179 |
. . . . . 6
β’ (π β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) supp (0gβπ
)) β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) supp (0gβπ
))) |
398 | 370, 371,
373, 394, 397 | fsuppsssuppgd 41061 |
. . . . 5
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) finSupp (0gβπ
)) |
399 | | eqid 2732 |
. . . . . 6
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π)) = (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π)) |
400 | 302, 13, 144, 399, 4, 16 | evlselvlem 41155 |
. . . . 5
β’ (π β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π)):({π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} Γ {π β (β0
βm π½)
β£ (β‘π β β) β Fin})β1-1-ontoβ{β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
401 | 28, 204, 296, 299, 368, 398, 400 | gsumf1o 19778 |
. . . 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} β¦ (π βͺ π))))) |
402 | 144 | psrbagf 21462 |
. . . . . . . . . 10
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β π:(πΌ β π½)βΆβ0) |
403 | 402 | ad2antrl 726 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π:(πΌ β π½)βΆβ0) |
404 | 13 | psrbagf 21462 |
. . . . . . . . . 10
β’ (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β π:π½βΆβ0) |
405 | 404 | ad2antll 727 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π:π½βΆβ0) |
406 | | disjdifr 4471 |
. . . . . . . . . 10
β’ ((πΌ β π½) β© π½) = β
|
407 | 406 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((πΌ β π½) β© π½) = β
) |
408 | 403, 405,
407 | fun2d 6752 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π βͺ π):((πΌ β π½) βͺ π½)βΆβ0) |
409 | | undifr 4481 |
. . . . . . . . . . 11
β’ (π½ β πΌ β ((πΌ β π½) βͺ π½) = πΌ) |
410 | 16, 409 | sylib 217 |
. . . . . . . . . 10
β’ (π β ((πΌ β π½) βͺ π½) = πΌ) |
411 | 410 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((πΌ β π½) βͺ π½) = πΌ) |
412 | 411 | feq2d 6700 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((π βͺ π):((πΌ β π½) βͺ π½)βΆβ0 β (π βͺ π):πΌβΆβ0)) |
413 | 408, 412 | mpbid 231 |
. . . . . . 7
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π βͺ π):πΌβΆβ0) |
414 | | vex 3478 |
. . . . . . . . . . 11
β’ π β V |
415 | | vex 3478 |
. . . . . . . . . . 11
β’ π β V |
416 | 414, 415 | unex 7729 |
. . . . . . . . . 10
β’ (π βͺ π) β V |
417 | 416 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π βͺ π) β V) |
418 | | 0zd 12566 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β 0
β β€) |
419 | 413 | ffund 6718 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β Fun
(π βͺ π)) |
420 | 144 | psrbagfsupp 21464 |
. . . . . . . . . . 11
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β π finSupp 0) |
421 | 420 | ad2antrl 726 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π finSupp 0) |
422 | 13 | psrbagfsupp 21464 |
. . . . . . . . . . 11
β’ (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β π finSupp 0) |
423 | 422 | ad2antll 727 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π finSupp 0) |
424 | 421, 423 | fsuppun 9378 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((π βͺ π) supp 0) β
Fin) |
425 | 417, 418,
419, 424 | isfsuppd 9362 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π βͺ π) finSupp 0) |
426 | | fcdmnn0fsuppg 12527 |
. . . . . . . . 9
β’ (((π βͺ π) β V β§ (π βͺ π):πΌβΆβ0) β ((π βͺ π) finSupp 0 β (β‘(π βͺ π) β β) β
Fin)) |
427 | 417, 413,
426 | syl2anc 584 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((π βͺ π) finSupp 0 β (β‘(π βͺ π) β β) β
Fin)) |
428 | 425, 427 | mpbid 231 |
. . . . . . 7
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (β‘(π βͺ π) β β) β
Fin) |
429 | 4 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β πΌ β π) |
430 | 302 | psrbag 21461 |
. . . . . . . 8
β’ (πΌ β π β ((π βͺ π) β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β ((π βͺ π):πΌβΆβ0 β§ (β‘(π βͺ π) β β) β
Fin))) |
431 | 429, 430 | syl 17 |
. . . . . . 7
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((π βͺ π) β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β ((π βͺ π):πΌβΆβ0 β§ (β‘(π βͺ π) β β) β
Fin))) |
432 | 413, 428,
431 | mpbir2and 711 |
. . . . . 6
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π βͺ π) β {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
433 | | eqidd 2733 |
. . . . . 6
β’ (π β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π)) = (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π))) |
434 | | eqidd 2733 |
. . . . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ))))))) |
435 | | reseq1 5973 |
. . . . . . . . . . . 12
β’ (π = (π βͺ π) β (π βΎ π½) = ((π βͺ π) βΎ π½)) |
436 | 435 | fveq2d 6892 |
. . . . . . . . . . 11
β’ (π = (π βͺ π) β ((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½)) = ((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½))) |
437 | | reseq1 5973 |
. . . . . . . . . . 11
β’ (π = (π βͺ π) β (π βΎ (πΌ β π½)) = ((π βͺ π) βΎ (πΌ β π½))) |
438 | 436, 437 | fveq12d 6895 |
. . . . . . . . . 10
β’ (π = (π βͺ π) β (((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½))) = (((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½))β((π βͺ π) βΎ (πΌ β π½)))) |
439 | 435 | fveq1d 6890 |
. . . . . . . . . . . . 13
β’ (π = (π βͺ π) β ((π βΎ π½)βπ) = (((π βͺ π) βΎ π½)βπ)) |
440 | 439 | oveq1d 7420 |
. . . . . . . . . . . 12
β’ (π = (π βͺ π) β (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) |
441 | 440 | mpteq2dv 5249 |
. . . . . . . . . . 11
β’ (π = (π βͺ π) β (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) = (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) |
442 | 441 | oveq2d 7421 |
. . . . . . . . . 10
β’ (π = (π βͺ π) β ((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) = ((mulGrpβπ
) Ξ£g (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) |
443 | 438, 442 | oveq12d 7423 |
. . . . . . . . 9
β’ (π = (π βͺ π) β ((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) = ((((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½))β((π βͺ π) βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
444 | 437 | fveq1d 6890 |
. . . . . . . . . . . 12
β’ (π = (π βͺ π) β ((π βΎ (πΌ β π½))βπ) = (((π βͺ π) βΎ (πΌ β π½))βπ)) |
445 | 444 | oveq1d 7420 |
. . . . . . . . . . 11
β’ (π = (π βͺ π) β (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) = ((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) |
446 | 445 | mpteq2dv 5249 |
. . . . . . . . . 10
β’ (π = (π βͺ π) β (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) = (π β (πΌ β π½) β¦ ((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) |
447 | 446 | oveq2d 7421 |
. . . . . . . . 9
β’ (π = (π βͺ π) β ((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) = ((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) |
448 | 443, 447 | oveq12d 7423 |
. . . . . . . 8
β’ (π = (π βͺ π) β (((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = (((((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½))β((π βͺ π) βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
449 | 416, 448 | csbie 3928 |
. . . . . . 7
β’
β¦(π
βͺ π) / πβ¦(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = (((((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½))β((π βͺ π) βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) |
450 | 402 | ffnd 6715 |
. . . . . . . . . . . . 13
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β π Fn (πΌ β π½)) |
451 | 450 | ad2antrl 726 |
. . . . . . . . . . . 12
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π Fn (πΌ β π½)) |
452 | 405 | ffnd 6715 |
. . . . . . . . . . . 12
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π Fn π½) |
453 | | fnunres2 6659 |
. . . . . . . . . . . 12
β’ ((π Fn (πΌ β π½) β§ π Fn π½ β§ ((πΌ β π½) β© π½) = β
) β ((π βͺ π) βΎ π½) = π) |
454 | 451, 452,
407, 453 | syl3anc 1371 |
. . . . . . . . . . 11
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((π βͺ π) βΎ π½) = π) |
455 | 454 | fveq2d 6892 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½)) = ((((πΌ selectVars π
)βπ½)βπΉ)βπ)) |
456 | | fnunres1 6658 |
. . . . . . . . . . 11
β’ ((π Fn (πΌ β π½) β§ π Fn π½ β§ ((πΌ β π½) β© π½) = β
) β ((π βͺ π) βΎ (πΌ β π½)) = π) |
457 | 451, 452,
407, 456 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((π βͺ π) βΎ (πΌ β π½)) = π) |
458 | 455, 457 | fveq12d 6895 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
(((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½))β((π βͺ π) βΎ (πΌ β π½))) = (((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)) |
459 | 454 | fveq1d 6890 |
. . . . . . . . . . . 12
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
(((π βͺ π) βΎ π½)βπ) = (πβπ)) |
460 | 459 | oveq1d 7420 |
. . . . . . . . . . 11
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) |
461 | 460 | mpteq2dv 5249 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) |
462 | 461 | oveq2d 7421 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((mulGrpβπ
)
Ξ£g (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) = ((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) |
463 | 458, 462 | oveq12d 7423 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((((((πΌ selectVars π
)βπ½)βπΉ)β((π βͺ π) βΎ π½))β((π βͺ π) βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((((π βͺ π) βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) = ((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))) |
464 | 457 | fveq1d 6890 |
. . . . . . . . . . 11
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
(((π βͺ π) βΎ (πΌ β π½))βπ) = (πβπ)) |
465 | 464 | oveq1d 7420 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) = ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) |
466 | 465 | mpteq2dv 5249 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π β (πΌ β π½) β¦ ((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) |
467 | 466 | oveq2d 7421 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((mulGrpβπ
)
Ξ£g (π β (πΌ β π½) β¦ ((((π βͺ π) βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) = ((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) |
468 | 463, 467 | oveq12d 7423 |
. . . . . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
469 | 449, 468 | eqtrid 2784 |
. . . . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
470 | 432, 433,
434, 469 | fmpocos 41053 |
. . . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ))))))) |
471 | 470 | oveq2d 7421 |
. . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ)))))))) |
472 | | ovex 7438 |
. . . . . . 7
β’
(β0 βm (πΌ β π½)) β V |
473 | 472 | rabex 5331 |
. . . . . 6
β’ {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β
V |
474 | 473 | a1i 11 |
. . . . 5
β’ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β
V) |
475 | 185 | a1i 11 |
. . . . 5
β’ (π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β
V) |
476 | 32 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π
β Ring) |
477 | 19 | ffvelcdmda 7083 |
. . . . . . . . . . . . 13
β’ ((π β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ)βπ) β (Baseβπ)) |
478 | 3, 28, 1, 144, 477 | mplelf 21548 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
((((πΌ selectVars π
)βπ½)βπΉ)βπ):{π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}βΆπΎ) |
479 | 478 | ffvelcdmda 7083 |
. . . . . . . . . . 11
β’ (((π β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) β πΎ) |
480 | 479 | an32s 650 |
. . . . . . . . . 10
β’ (((π β§ π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}) β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin}) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) β πΎ) |
481 | 480 | anasss 467 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
(((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ) β πΎ) |
482 | 24 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π½ β V) |
483 | 7 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π
β CRing) |
484 | 36 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π΄ βΎ π½) β (πΎ βm π½)) |
485 | | simprr 771 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π β {π β (β0
βm π½)
β£ (β‘π β β) β
Fin}) |
486 | 13, 28, 47, 49, 482, 483, 484, 485 | evlsvvvallem 41130 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((mulGrpβπ
)
Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) β πΎ) |
487 | 28, 143, 476, 481, 486 | ringcld 20073 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) β πΎ) |
488 | 6 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (πΌ β π½) β V) |
489 | 35, 5 | elmapssresd 41063 |
. . . . . . . . . 10
β’ (π β (π΄ βΎ (πΌ β π½)) β (πΎ βm (πΌ β π½))) |
490 | 489 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β (π΄ βΎ (πΌ β π½)) β (πΎ βm (πΌ β π½))) |
491 | | simprl 769 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β
Fin}) |
492 | 144, 28, 47, 49, 488, 483, 490, 491 | evlsvvvallem 41130 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
((mulGrpβπ
)
Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) β πΎ) |
493 | 28, 143, 476, 487, 492 | ringcld 20073 |
. . . . . . 7
β’ ((π β§ (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β§ π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin})) β
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) β πΎ) |
494 | 493 | ralrimivva 3200 |
. . . . . 6
β’ (π β βπ β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}βπ β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} (((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) β πΎ) |
495 | 287 | fmpo 8050 |
. . . . . 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})βΆπΎ) |
496 | 494, 495 | 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})βΆπΎ) |
497 | | f1of1 6829 |
. . . . . . . 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}) |
498 | 400, 497 | syl 17 |
. . . . . . 7
β’ (π β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π)):({π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} Γ {π β (β0
βm π½)
β£ (β‘π β β) β Fin})β1-1β{β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
499 | 398, 498,
371, 370 | fsuppco 9393 |
. . . . . 6
β’ (π β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦ (π βͺ π))) finSupp (0gβπ
)) |
500 | 470, 499 | eqbrtrrd 5171 |
. . . . 5
β’ (π β (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin}, π β {π β (β0
βm π½)
β£ (β‘π β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)βπ)βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) finSupp (0gβπ
)) |
501 | 28, 204, 296, 474, 475, 496, 500 | gsumxp 19838 |
. . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ))))))π)))))) |
502 | 401, 471,
501 | 3eqtrd 2776 |
. . 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βπ
))((π΄ βΎ (πΌ β π½))βπ))))))π)))))) |
503 | 28, 143, 300, 311, 342, 366 | ringassd 20072 |
. . . . . 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βπ
))((π΄ βΎ (πΌ β π½))βπ))))))) |
504 | 47, 143 | mgpplusg 19985 |
. . . . . . . . 9
β’
(.rβπ
) = (+gβ(mulGrpβπ
)) |
505 | 51 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β (mulGrpβπ
) β Mnd) |
506 | 316 | ffvelcdmda 7083 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β (πβπ) β
β0) |
507 | 57 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π΄:πΌβΆπΎ) |
508 | 507 | ffvelcdmda 7083 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β (π΄βπ) β πΎ) |
509 | 48, 49, 505, 506, 508 | mulgnn0cld 18969 |
. . . . . . . . . 10
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)) β πΎ) |
510 | 509 | fmpttd 7111 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))):πΌβΆπΎ) |
511 | 4 | mptexd 7222 |
. . . . . . . . . . 11
β’ (π β (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) β V) |
512 | 511 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) β V) |
513 | | funmpt 6583 |
. . . . . . . . . . 11
β’ Fun
(π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) |
514 | 513 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β Fun
(π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))) |
515 | 316 | feqmptd 6957 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π = (π β πΌ β¦ (πβπ))) |
516 | 515, 329 | eqbrtrrd 5171 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β πΌ β¦ (πβπ)) finSupp 0) |
517 | | ssidd 4004 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β πΌ β¦ (πβπ)) supp 0) β ((π β πΌ β¦ (πβπ)) supp 0)) |
518 | 117 | adantl 482 |
. . . . . . . . . . 11
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΎ) β
(0(.gβ(mulGrpβπ
))π) = (0gβ(mulGrpβπ
))) |
519 | 517, 518,
506, 508, 330 | suppssov1 8179 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) supp
(0gβ(mulGrpβπ
))) β ((π β πΌ β¦ (πβπ)) supp 0)) |
520 | 512, 325,
514, 516, 519 | fsuppsssuppgd 41061 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) finSupp
(0gβ(mulGrpβπ
))) |
521 | | disjdif 4470 |
. . . . . . . . . 10
β’ (π½ β© (πΌ β π½)) = β
|
522 | 521 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π½ β© (πΌ β π½)) = β
) |
523 | | undif 4480 |
. . . . . . . . . . . 12
β’ (π½ β πΌ β (π½ βͺ (πΌ β π½)) = πΌ) |
524 | 16, 523 | sylib 217 |
. . . . . . . . . . 11
β’ (π β (π½ βͺ (πΌ β π½)) = πΌ) |
525 | 524 | eqcomd 2738 |
. . . . . . . . . 10
β’ (π β πΌ = (π½ βͺ (πΌ β π½))) |
526 | 525 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β πΌ = (π½ βͺ (πΌ β π½))) |
527 | 48, 116, 504, 312, 303, 510, 520, 522, 526 | gsumsplit 19790 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((mulGrpβπ
)
Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))) = (((mulGrpβπ
) Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ π½))(.rβπ
)((mulGrpβπ
) Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ (πΌ β π½))))) |
528 | 304 | resmptd 6038 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ π½) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))) |
529 | | fveq2 6888 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβπ) = (πβπ)) |
530 | | fveq2 6888 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΄βπ) = (π΄βπ)) |
531 | 529, 530 | oveq12d 7423 |
. . . . . . . . . . . . 13
β’ (π = π β ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)) = ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) |
532 | 531 | cbvmptv 5260 |
. . . . . . . . . . . 12
β’ (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) = (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) |
533 | | simpr 485 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β π β π½) |
534 | 533 | fvresd 6908 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β ((π βΎ π½)βπ) = (πβπ)) |
535 | 533 | fvresd 6908 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β ((π΄ βΎ π½)βπ) = (π΄βπ)) |
536 | 534, 535 | oveq12d 7423 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)) = ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) |
537 | 536 | eqcomd 2738 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β π½) β ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)) = (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))) |
538 | 537 | mpteq2dva 5247 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) = (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) |
539 | 532, 538 | eqtrid 2784 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β π½ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) = (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) |
540 | 528, 539 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ π½) = (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))) |
541 | 540 | oveq2d 7421 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((mulGrpβπ
)
Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ π½)) = ((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))) |
542 | 309 | resmptd 6038 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ (πΌ β π½)) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))) |
543 | | fveq2 6888 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβπ) = (πβπ)) |
544 | | fveq2 6888 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΄βπ) = (π΄βπ)) |
545 | 543, 544 | oveq12d 7423 |
. . . . . . . . . . . . 13
β’ (π = π β ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)) = ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) |
546 | 545 | cbvmptv 5260 |
. . . . . . . . . . . 12
β’ (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) = (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) |
547 | | simpr 485 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β π β (πΌ β π½)) |
548 | 547 | fvresd 6908 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β ((π βΎ (πΌ β π½))βπ) = (πβπ)) |
549 | 547 | fvresd 6908 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β ((π΄ βΎ (πΌ β π½))βπ) = (π΄βπ)) |
550 | 548, 549 | oveq12d 7423 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)) = ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) |
551 | 550 | eqcomd 2738 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β (πΌ β π½)) β ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)) = (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))) |
552 | 551 | mpteq2dva 5247 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) = (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) |
553 | 546, 552 | eqtrid 2784 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) = (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) |
554 | 542, 553 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ (πΌ β π½)) = (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))) |
555 | 554 | oveq2d 7421 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((mulGrpβπ
)
Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ (πΌ β π½))) = ((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) |
556 | 541, 555 | oveq12d 7423 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(((mulGrpβπ
)
Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ π½))(.rβπ
)((mulGrpβπ
) Ξ£g ((π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))) βΎ (πΌ β π½)))) = (((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) |
557 | 527, 556 | eqtr2d 2773 |
. . . . . . 7
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(((mulGrpβπ
)
Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = ((mulGrpβπ
) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))))) |
558 | 380, 557 | oveq12d 7423 |
. . . . . 6
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)(((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) = ((πΉβπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))))) |
559 | 503, 558 | eqtrd 2772 |
. . . . 5
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))) = ((πΉβπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))))) |
560 | 559 | mpteq2dva 5247 |
. . . 4
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦
(((((((πΌ selectVars π
)βπ½)βπΉ)β(π βΎ π½))β(π βΎ (πΌ β π½)))(.rβπ
)((mulGrpβπ
) Ξ£g (π β π½ β¦ (((π βΎ π½)βπ)(.gβ(mulGrpβπ
))((π΄ βΎ π½)βπ)))))(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ (((π βΎ (πΌ β π½))βπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))) = (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ ((πΉβπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ))))))) |
561 | 560 | oveq2d 7421 |
. . 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βπ
))(π΄βπ)))))))) |
562 | 295, 502,
561 | 3eqtr2d 2778 |
. 2
β’ (π β (π
Ξ£g (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β¦
(((((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½)))βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ))))))) = (π
Ξ£g (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ ((πΉβπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))))))) |
563 | | eqid 2732 |
. . 3
β’ ((πΌ β π½) eval π
) = ((πΌ β π½) eval π
) |
564 | 563, 3, 1, 144, 28, 47, 49, 143, 6, 7, 173, 489 | evlvvval 41142 |
. 2
β’ (π β ((((πΌ β π½) eval π
)β(((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½))))β(π΄ βΎ (πΌ β π½))) = (π
Ξ£g (π β {π β (β0
βm (πΌ
β π½)) β£ (β‘π β β) β Fin} β¦
(((((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½)))βπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β (πΌ β π½) β¦ ((πβπ)(.gβ(mulGrpβπ
))((π΄ βΎ (πΌ β π½))βπ)))))))) |
565 | | eqid 2732 |
. . 3
β’ (πΌ eval π
) = (πΌ eval π
) |
566 | 565, 14, 15, 302, 28, 47, 49, 143, 4, 7, 17, 35 | evlvvval 41142 |
. 2
β’ (π β (((πΌ eval π
)βπΉ)βπ΄) = (π
Ξ£g (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ ((πΉβπ)(.rβπ
)((mulGrpβπ
) Ξ£g (π β πΌ β¦ ((πβπ)(.gβ(mulGrpβπ
))(π΄βπ)))))))) |
567 | 562, 564,
566 | 3eqtr4d 2782 |
1
β’ (π β ((((πΌ β π½) eval π
)β(((π½ eval π)β(((πΌ selectVars π
)βπ½)βπΉ))β(πΏ β (π΄ βΎ π½))))β(π΄ βΎ (πΌ β π½))) = (((πΌ eval π
)βπΉ)βπ΄)) |