Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ
) |
2 | | eqid 2733 |
. . . . 5
β’
(0gβπ
) = (0gβπ
) |
3 | | psrmulcl.r |
. . . . . . 7
β’ (π β π
β Ring) |
4 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π·) β π
β Ring) |
5 | 4 | ringcmnd 20010 |
. . . . 5
β’ ((π β§ π β π·) β π
β CMnd) |
6 | | psrmulcl.d |
. . . . . . 7
β’ π· = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
7 | 6 | psrbaglefi 21350 |
. . . . . 6
β’ (π β π· β {π¦ β π· β£ π¦ βr β€ π} β Fin) |
8 | 7 | adantl 483 |
. . . . 5
β’ ((π β§ π β π·) β {π¦ β π· β£ π¦ βr β€ π} β Fin) |
9 | | eqid 2733 |
. . . . . . 7
β’
(.rβπ
) = (.rβπ
) |
10 | 3 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β π·) β§ π₯ β {π¦ β π· β£ π¦ βr β€ π}) β π
β Ring) |
11 | | psrmulcl.s |
. . . . . . . . . 10
β’ π = (πΌ mPwSer π
) |
12 | | psrmulcl.b |
. . . . . . . . . 10
β’ π΅ = (Baseβπ) |
13 | | psrmulcl.x |
. . . . . . . . . 10
β’ (π β π β π΅) |
14 | 11, 1, 6, 12, 13 | psrelbas 21363 |
. . . . . . . . 9
β’ (π β π:π·βΆ(Baseβπ
)) |
15 | 14 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π₯ β {π¦ β π· β£ π¦ βr β€ π}) β π:π·βΆ(Baseβπ
)) |
16 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π₯ β {π¦ β π· β£ π¦ βr β€ π}) β π₯ β {π¦ β π· β£ π¦ βr β€ π}) |
17 | | breq1 5109 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β (π¦ βr β€ π β π₯ βr β€ π)) |
18 | 17 | elrab 3646 |
. . . . . . . . . 10
β’ (π₯ β {π¦ β π· β£ π¦ βr β€ π} β (π₯ β π· β§ π₯ βr β€ π)) |
19 | 16, 18 | sylib 217 |
. . . . . . . . 9
β’ (((π β§ π β π·) β§ π₯ β {π¦ β π· β£ π¦ βr β€ π}) β (π₯ β π· β§ π₯ βr β€ π)) |
20 | 19 | simpld 496 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π₯ β {π¦ β π· β£ π¦ βr β€ π}) β π₯ β π·) |
21 | 15, 20 | ffvelcdmd 7037 |
. . . . . . 7
β’ (((π β§ π β π·) β§ π₯ β {π¦ β π· β£ π¦ βr β€ π}) β (πβπ₯) β (Baseβπ
)) |
22 | | psrmulcl.y |
. . . . . . . . . 10
β’ (π β π β π΅) |
23 | 11, 1, 6, 12, 22 | psrelbas 21363 |
. . . . . . . . 9
β’ (π β π:π·βΆ(Baseβπ
)) |
24 | 23 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π₯ β {π¦ β π· β£ π¦ βr β€ π}) β π:π·βΆ(Baseβπ
)) |
25 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π₯ β {π¦ β π· β£ π¦ βr β€ π}) β π β π·) |
26 | 6 | psrbagf 21336 |
. . . . . . . . . . 11
β’ (π₯ β π· β π₯:πΌβΆβ0) |
27 | 20, 26 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π₯ β {π¦ β π· β£ π¦ βr β€ π}) β π₯:πΌβΆβ0) |
28 | 19 | simprd 497 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π₯ β {π¦ β π· β£ π¦ βr β€ π}) β π₯ βr β€ π) |
29 | 6 | psrbagcon 21348 |
. . . . . . . . . 10
β’ ((π β π· β§ π₯:πΌβΆβ0 β§ π₯ βr β€ π) β ((π βf β π₯) β π· β§ (π βf β π₯) βr β€ π)) |
30 | 25, 27, 28, 29 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ π β π·) β§ π₯ β {π¦ β π· β£ π¦ βr β€ π}) β ((π βf β π₯) β π· β§ (π βf β π₯) βr β€ π)) |
31 | 30 | simpld 496 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π₯ β {π¦ β π· β£ π¦ βr β€ π}) β (π βf β π₯) β π·) |
32 | 24, 31 | ffvelcdmd 7037 |
. . . . . . 7
β’ (((π β§ π β π·) β§ π₯ β {π¦ β π· β£ π¦ βr β€ π}) β (πβ(π βf β π₯)) β (Baseβπ
)) |
33 | 1, 9, 10, 21, 32 | ringcld 19991 |
. . . . . 6
β’ (((π β§ π β π·) β§ π₯ β {π¦ β π· β£ π¦ βr β€ π}) β ((πβπ₯)(.rβπ
)(πβ(π βf β π₯))) β (Baseβπ
)) |
34 | 33 | fmpttd 7064 |
. . . . 5
β’ ((π β§ π β π·) β (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))):{π¦ β π· β£ π¦ βr β€ π}βΆ(Baseβπ
)) |
35 | | fvexd 6858 |
. . . . . 6
β’ ((π β§ π β π·) β (0gβπ
) β V) |
36 | 34, 8, 35 | fdmfifsupp 9320 |
. . . . 5
β’ ((π β§ π β π·) β (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))) finSupp
(0gβπ
)) |
37 | 1, 2, 5, 8, 34, 36 | gsumcl 19697 |
. . . 4
β’ ((π β§ π β π·) β (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯))))) β (Baseβπ
)) |
38 | 37 | fmpttd 7064 |
. . 3
β’ (π β (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))))):π·βΆ(Baseβπ
)) |
39 | | fvex 6856 |
. . . 4
β’
(Baseβπ
)
β V |
40 | | ovex 7391 |
. . . . 5
β’
(β0 βm πΌ) β V |
41 | 6, 40 | rabex2 5292 |
. . . 4
β’ π· β V |
42 | 39, 41 | elmap 8812 |
. . 3
β’ ((π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))))) β ((Baseβπ
) βm π·) β (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))))):π·βΆ(Baseβπ
)) |
43 | 38, 42 | sylibr 233 |
. 2
β’ (π β (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))))) β ((Baseβπ
) βm π·)) |
44 | | psrmulcl.t |
. . 3
β’ Β· =
(.rβπ) |
45 | 11, 12, 9, 44, 6, 13, 22 | psrmulfval 21369 |
. 2
β’ (π β (π Β· π) = (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯))))))) |
46 | | reldmpsr 21332 |
. . . . . 6
β’ Rel dom
mPwSer |
47 | 46, 11, 12 | elbasov 17095 |
. . . . 5
β’ (π β π΅ β (πΌ β V β§ π
β V)) |
48 | 13, 47 | syl 17 |
. . . 4
β’ (π β (πΌ β V β§ π
β V)) |
49 | 48 | simpld 496 |
. . 3
β’ (π β πΌ β V) |
50 | 11, 1, 6, 12, 49 | psrbas 21362 |
. 2
β’ (π β π΅ = ((Baseβπ
) βm π·)) |
51 | 43, 45, 50 | 3eltr4d 2849 |
1
β’ (π β (π Β· π) β π΅) |