Step | Hyp | Ref
| Expression |
1 | | eqid 2736 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ
) |
2 | | eqid 2736 |
. . . . 5
β’
(0gβπ
) = (0gβπ
) |
3 | | ringcmn 19861 |
. . . . . . 7
β’ (π
β Ring β π
β CMnd) |
4 | 3 | 3ad2ant1 1133 |
. . . . . 6
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β π
β CMnd) |
5 | 4 | adantr 482 |
. . . . 5
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β π
β CMnd) |
6 | | ovex 7336 |
. . . . . . . 8
β’
(β0 βm πΌ) β V |
7 | 6 | rabex 5265 |
. . . . . . 7
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β
V |
8 | 7 | rabex 5265 |
. . . . . 6
β’ {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β V |
9 | 8 | a1i 11 |
. . . . 5
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β V) |
10 | | simpll1 1212 |
. . . . . . 7
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β π
β Ring) |
11 | | psropprmul.y |
. . . . . . . . . 10
β’ π = (πΌ mPwSer π
) |
12 | | eqid 2736 |
. . . . . . . . . 10
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
13 | | psropprmul.b |
. . . . . . . . . 10
β’ π΅ = (Baseβπ) |
14 | | simp3 1138 |
. . . . . . . . . 10
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β πΊ β π΅) |
15 | 11, 1, 12, 13, 14 | psrelbas 21189 |
. . . . . . . . 9
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β πΊ:{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ
)) |
16 | 15 | adantr 482 |
. . . . . . . 8
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β πΊ:{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ
)) |
17 | | elrabi 3623 |
. . . . . . . 8
β’ (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β π β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
18 | | ffvelcdm 6987 |
. . . . . . . 8
β’ ((πΊ:{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ
)
β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (πΊβπ) β (Baseβπ
)) |
19 | 16, 17, 18 | syl2an 597 |
. . . . . . 7
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β (πΊβπ) β (Baseβπ
)) |
20 | | simp2 1137 |
. . . . . . . . . 10
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β πΉ β π΅) |
21 | 11, 1, 12, 13, 20 | psrelbas 21189 |
. . . . . . . . 9
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β πΉ:{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ
)) |
22 | 21 | ad2antrr 724 |
. . . . . . . 8
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β πΉ:{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ
)) |
23 | | ssrab2 4019 |
. . . . . . . . 9
β’ {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
24 | | eqid 2736 |
. . . . . . . . . . 11
β’ {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} = {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} |
25 | 12, 24 | psrbagconcl 21178 |
. . . . . . . . . 10
β’ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β (π βf β π) β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) |
26 | 25 | adantll 712 |
. . . . . . . . 9
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β (π βf β π) β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) |
27 | 23, 26 | sselid 3924 |
. . . . . . . 8
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β (π βf β π) β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
28 | 22, 27 | ffvelcdmd 6990 |
. . . . . . 7
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β (πΉβ(π βf β π)) β (Baseβπ
)) |
29 | | eqid 2736 |
. . . . . . . 8
β’
(.rβπ
) = (.rβπ
) |
30 | 1, 29 | ringcl 19841 |
. . . . . . 7
β’ ((π
β Ring β§ (πΊβπ) β (Baseβπ
) β§ (πΉβ(π βf β π)) β (Baseβπ
)) β ((πΊβπ)(.rβπ
)(πΉβ(π βf β π))) β (Baseβπ
)) |
31 | 10, 19, 28, 30 | syl3anc 1371 |
. . . . . 6
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β ((πΊβπ)(.rβπ
)(πΉβ(π βf β π))) β (Baseβπ
)) |
32 | 31 | fmpttd 7017 |
. . . . 5
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))):{π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}βΆ(Baseβπ
)) |
33 | | mptexg 7125 |
. . . . . . 7
β’ ({π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β V β (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) β V) |
34 | 8, 33 | mp1i 13 |
. . . . . 6
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) β V) |
35 | | funmpt 6497 |
. . . . . . 7
β’ Fun
(π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) |
36 | 35 | a1i 11 |
. . . . . 6
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β Fun
(π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π))))) |
37 | | fvexd 6815 |
. . . . . 6
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
(0gβπ
)
β V) |
38 | 12 | psrbaglefi 21176 |
. . . . . . 7
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β Fin) |
39 | 38 | adantl 483 |
. . . . . 6
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β Fin) |
40 | | suppssdm 8020 |
. . . . . . . 8
β’ ((π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) supp
(0gβπ
))
β dom (π β
{π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) |
41 | | eqid 2736 |
. . . . . . . . 9
β’ (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) = (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) |
42 | 41 | dmmptss 6155 |
. . . . . . . 8
β’ dom
(π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} |
43 | 40, 42 | sstri 3935 |
. . . . . . 7
β’ ((π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) supp
(0gβπ
))
β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} |
44 | 43 | a1i 11 |
. . . . . 6
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) supp
(0gβπ
))
β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) |
45 | | suppssfifsupp 9183 |
. . . . . 6
β’ ((((π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) β V β§ Fun (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) β§
(0gβπ
)
β V) β§ ({π β
{π β
(β0 βm πΌ) β£ (β‘π β β) β Fin} β£ π βr β€ π} β Fin β§ ((π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) supp
(0gβπ
))
β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π})) β (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) finSupp
(0gβπ
)) |
46 | 34, 36, 37, 39, 44, 45 | syl32anc 1378 |
. . . . 5
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) finSupp
(0gβπ
)) |
47 | 12, 24 | psrbagconf1o 21180 |
. . . . . 6
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ (π βf β π)):{π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}β1-1-ontoβ{π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) |
48 | 47 | adantl 483 |
. . . . 5
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ (π βf β π)):{π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}β1-1-ontoβ{π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) |
49 | 1, 2, 5, 9, 32, 46, 48 | gsumf1o 19558 |
. . . 4
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π
Ξ£g
(π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π))))) = (π
Ξ£g ((π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) β (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ (π βf β π))))) |
50 | 12, 24 | psrbagconcl 21178 |
. . . . . . . 8
β’ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β (π βf β π) β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) |
51 | 50 | adantll 712 |
. . . . . . 7
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β (π βf β π) β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) |
52 | | eqidd 2737 |
. . . . . . 7
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ (π βf β π)) = (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ (π βf β π))) |
53 | | eqidd 2737 |
. . . . . . 7
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) = (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π))))) |
54 | | fveq2 6800 |
. . . . . . . 8
β’ (π = (π βf β π) β (πΊβπ) = (πΊβ(π βf β π))) |
55 | | oveq2 7311 |
. . . . . . . . 9
β’ (π = (π βf β π) β (π βf β π) = (π βf β (π βf β
π))) |
56 | 55 | fveq2d 6804 |
. . . . . . . 8
β’ (π = (π βf β π) β (πΉβ(π βf β π)) = (πΉβ(π βf β (π βf β
π)))) |
57 | 54, 56 | oveq12d 7321 |
. . . . . . 7
β’ (π = (π βf β π) β ((πΊβπ)(.rβπ
)(πΉβ(π βf β π))) = ((πΊβ(π βf β π))(.rβπ
)(πΉβ(π βf β (π βf β
π))))) |
58 | 51, 52, 53, 57 | fmptco 7029 |
. . . . . 6
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) β (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ (π βf β π))) = (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβ(π βf β π))(.rβπ
)(πΉβ(π βf β (π βf β
π)))))) |
59 | | reldmpsr 21158 |
. . . . . . . . . . . . . 14
β’ Rel dom
mPwSer |
60 | 11, 13, 59 | strov2rcl 16961 |
. . . . . . . . . . . . 13
β’ (πΊ β π΅ β πΌ β V) |
61 | 60 | 3ad2ant3 1135 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β πΌ β V) |
62 | 61 | ad2antrr 724 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β πΌ β V) |
63 | 12 | psrbagf 21162 |
. . . . . . . . . . . . 13
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β π:πΌβΆβ0) |
64 | 63 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β π:πΌβΆβ0) |
65 | 64 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β π:πΌβΆβ0) |
66 | | elrabi 3623 |
. . . . . . . . . . . . 13
β’ (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β π β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
67 | 12 | psrbagf 21162 |
. . . . . . . . . . . . 13
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β π:πΌβΆβ0) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . 12
β’ (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β π:πΌβΆβ0) |
69 | 68 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β π:πΌβΆβ0) |
70 | | nn0cn 12285 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β) |
71 | | nn0cn 12285 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β) |
72 | | nncan 11292 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β) β (π β (π β π)) = π) |
73 | 70, 71, 72 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π β
β0) β (π β (π β π)) = π) |
74 | 73 | adantl 483 |
. . . . . . . . . . 11
β’
(((((π
β Ring
β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β§ (π β β0 β§ π β β0))
β (π β (π β π)) = π) |
75 | 62, 65, 69, 74 | caonncan 7602 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β (π βf β (π βf β
π)) = π) |
76 | 75 | fveq2d 6804 |
. . . . . . . . 9
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β (πΉβ(π βf β (π βf β
π))) = (πΉβπ)) |
77 | 76 | oveq2d 7319 |
. . . . . . . 8
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β ((πΊβ(π βf β π))(.rβπ
)(πΉβ(π βf β (π βf β
π)))) = ((πΊβ(π βf β π))(.rβπ
)(πΉβπ))) |
78 | | psropprmul.s |
. . . . . . . . 9
β’ π =
(opprβπ
) |
79 | | eqid 2736 |
. . . . . . . . 9
β’
(.rβπ) = (.rβπ) |
80 | 1, 29, 78, 79 | opprmul 19906 |
. . . . . . . 8
β’ ((πΉβπ)(.rβπ)(πΊβ(π βf β π))) = ((πΊβ(π βf β π))(.rβπ
)(πΉβπ)) |
81 | 77, 80 | eqtr4di 2794 |
. . . . . . 7
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π}) β ((πΊβ(π βf β π))(.rβπ
)(πΉβ(π βf β (π βf β
π)))) = ((πΉβπ)(.rβπ)(πΊβ(π βf β π)))) |
82 | 81 | mpteq2dva 5181 |
. . . . . 6
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβ(π βf β π))(.rβπ
)(πΉβ(π βf β (π βf β
π))))) = (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ)(πΊβ(π βf β π))))) |
83 | 58, 82 | eqtrd 2776 |
. . . . 5
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) β (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ (π βf β π))) = (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ)(πΊβ(π βf β π))))) |
84 | 83 | oveq2d 7319 |
. . . 4
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π
Ξ£g
((π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))) β (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ (π βf β π)))) = (π
Ξ£g (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ)(πΊβ(π βf β π)))))) |
85 | 8 | mptex 7127 |
. . . . . . . 8
β’ (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ)(πΊβ(π βf β π)))) β V |
86 | 85 | a1i 11 |
. . . . . . 7
β’ (π
β Ring β (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ)(πΊβ(π βf β π)))) β V) |
87 | | id 22 |
. . . . . . 7
β’ (π
β Ring β π
β Ring) |
88 | 78 | fvexi 6814 |
. . . . . . . 8
β’ π β V |
89 | 88 | a1i 11 |
. . . . . . 7
β’ (π
β Ring β π β V) |
90 | 78, 1 | opprbas 19910 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ) |
91 | 90 | a1i 11 |
. . . . . . 7
β’ (π
β Ring β
(Baseβπ
) =
(Baseβπ)) |
92 | | eqid 2736 |
. . . . . . . . 9
β’
(+gβπ
) = (+gβπ
) |
93 | 78, 92 | oppradd 19912 |
. . . . . . . 8
β’
(+gβπ
) = (+gβπ) |
94 | 93 | a1i 11 |
. . . . . . 7
β’ (π
β Ring β
(+gβπ
) =
(+gβπ)) |
95 | 86, 87, 89, 91, 94 | gsumpropd 18403 |
. . . . . 6
β’ (π
β Ring β (π
Ξ£g
(π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ)(πΊβ(π βf β π))))) = (π Ξ£g (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ)(πΊβ(π βf β π)))))) |
96 | 95 | 3ad2ant1 1133 |
. . . . 5
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (π
Ξ£g (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ)(πΊβ(π βf β π))))) = (π Ξ£g (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ)(πΊβ(π βf β π)))))) |
97 | 96 | adantr 482 |
. . . 4
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π
Ξ£g
(π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ)(πΊβ(π βf β π))))) = (π Ξ£g (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ)(πΊβ(π βf β π)))))) |
98 | 49, 84, 97 | 3eqtrd 2780 |
. . 3
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π
Ξ£g
(π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π))))) = (π Ξ£g (π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ)(πΊβ(π βf β π)))))) |
99 | 98 | mpteq2dva 5181 |
. 2
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ (π
Ξ£g
(π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π)))))) = (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ (π Ξ£g
(π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ)(πΊβ(π βf β π))))))) |
100 | | psropprmul.t |
. . 3
β’ Β· =
(.rβπ) |
101 | 11, 13, 29, 100, 12, 14, 20 | psrmulfval 21195 |
. 2
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (πΊ Β· πΉ) = (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ (π
Ξ£g
(π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΊβπ)(.rβπ
)(πΉβ(π βf β π))))))) |
102 | | psropprmul.z |
. . 3
β’ π = (πΌ mPwSer π) |
103 | | eqid 2736 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
104 | | psropprmul.u |
. . 3
β’ β =
(.rβπ) |
105 | 90 | a1i 11 |
. . . . . 6
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (Baseβπ
) = (Baseβπ)) |
106 | 105 | psrbaspropd 21447 |
. . . . 5
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (Baseβ(πΌ mPwSer π
)) = (Baseβ(πΌ mPwSer π))) |
107 | 11 | fveq2i 6803 |
. . . . . 6
β’
(Baseβπ) =
(Baseβ(πΌ mPwSer π
)) |
108 | 13, 107 | eqtri 2764 |
. . . . 5
β’ π΅ = (Baseβ(πΌ mPwSer π
)) |
109 | 102 | fveq2i 6803 |
. . . . 5
β’
(Baseβπ) =
(Baseβ(πΌ mPwSer π)) |
110 | 106, 108,
109 | 3eqtr4g 2801 |
. . . 4
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β π΅ = (Baseβπ)) |
111 | 20, 110 | eleqtrd 2839 |
. . 3
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β πΉ β (Baseβπ)) |
112 | 14, 110 | eleqtrd 2839 |
. . 3
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β πΊ β (Baseβπ)) |
113 | 102, 103,
79, 104, 12, 111, 112 | psrmulfval 21195 |
. 2
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (πΉ β πΊ) = (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ (π Ξ£g
(π β {π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ)(πΊβ(π βf β π))))))) |
114 | 99, 101, 113 | 3eqtr4rd 2787 |
1
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (πΉ β πΊ) = (πΊ Β· πΉ)) |