Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . . 8
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
2 | 1 | psrbaglefi 21357 |
. . . . . . 7
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β Fin) |
3 | 2 | adantl 483 |
. . . . . 6
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β Fin) |
4 | | resspsr.2 |
. . . . . . . . 9
β’ (π β π β (SubRingβπ
)) |
5 | | subrgsubg 20270 |
. . . . . . . . 9
β’ (π β (SubRingβπ
) β π β (SubGrpβπ
)) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
β’ (π β π β (SubGrpβπ
)) |
7 | | subgsubm 18958 |
. . . . . . . 8
β’ (π β (SubGrpβπ
) β π β (SubMndβπ
)) |
8 | 6, 7 | syl 17 |
. . . . . . 7
β’ (π β π β (SubMndβπ
)) |
9 | 8 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β π β (SubMndβπ
)) |
10 | 4 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) β π β (SubRingβπ
)) |
11 | | resspsr.u |
. . . . . . . . . . . 12
β’ π = (πΌ mPwSer π») |
12 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Baseβπ») =
(Baseβπ») |
13 | | resspsr.b |
. . . . . . . . . . . 12
β’ π΅ = (Baseβπ) |
14 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π΅) |
15 | 11, 12, 1, 13, 14 | psrelbas 21370 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅)) β π:{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ»)) |
16 | 15 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β π:{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ»)) |
17 | | elrabi 3643 |
. . . . . . . . . 10
β’ (π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
18 | | ffvelcdm 7036 |
. . . . . . . . . 10
β’ ((π:{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ»)
β§ π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (πβπ₯) β (Baseβπ»)) |
19 | 16, 17, 18 | syl2an 597 |
. . . . . . . . 9
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) β (πβπ₯) β (Baseβπ»)) |
20 | | resspsr.h |
. . . . . . . . . . 11
β’ π» = (π
βΎs π) |
21 | 20 | subrgbas 20273 |
. . . . . . . . . 10
β’ (π β (SubRingβπ
) β π = (Baseβπ»)) |
22 | 10, 21 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) β π = (Baseβπ»)) |
23 | 19, 22 | eleqtrrd 2837 |
. . . . . . . 8
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) β (πβπ₯) β π) |
24 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π΅) |
25 | 11, 12, 1, 13, 24 | psrelbas 21370 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅)) β π:{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ»)) |
26 | 25 | ad2antrr 725 |
. . . . . . . . . 10
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) β π:{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ»)) |
27 | | ssrab2 4041 |
. . . . . . . . . . 11
β’ {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
28 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) β π β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
29 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) β π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) |
30 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} = {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} |
31 | 1, 30 | psrbagconcl 21359 |
. . . . . . . . . . . 12
β’ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) β (π βf β π₯) β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) |
32 | 28, 29, 31 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) β (π βf β π₯) β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) |
33 | 27, 32 | sselid 3946 |
. . . . . . . . . 10
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) β (π βf β π₯) β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
34 | 26, 33 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) β (πβ(π βf β π₯)) β (Baseβπ»)) |
35 | 34, 22 | eleqtrrd 2837 |
. . . . . . . 8
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) β (πβ(π βf β π₯)) β π) |
36 | | eqid 2733 |
. . . . . . . . 9
β’
(.rβπ
) = (.rβπ
) |
37 | 36 | subrgmcl 20276 |
. . . . . . . 8
β’ ((π β (SubRingβπ
) β§ (πβπ₯) β π β§ (πβ(π βf β π₯)) β π) β ((πβπ₯)(.rβπ
)(πβ(π βf β π₯))) β π) |
38 | 10, 23, 35, 37 | syl3anc 1372 |
. . . . . . 7
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) β ((πβπ₯)(.rβπ
)(πβ(π βf β π₯))) β π) |
39 | 38 | fmpttd 7067 |
. . . . . 6
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))):{π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}βΆπ) |
40 | 3, 9, 39, 20 | gsumsubm 18653 |
. . . . 5
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π
Ξ£g
(π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯))))) = (π» Ξ£g (π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))))) |
41 | 20, 36 | ressmulr 17196 |
. . . . . . . . . 10
β’ (π β (SubRingβπ
) β
(.rβπ
) =
(.rβπ»)) |
42 | 4, 41 | syl 17 |
. . . . . . . . 9
β’ (π β (.rβπ
) = (.rβπ»)) |
43 | 42 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) β
(.rβπ
) =
(.rβπ»)) |
44 | 43 | oveqd 7378 |
. . . . . . 7
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π}) β ((πβπ₯)(.rβπ
)(πβ(π βf β π₯))) = ((πβπ₯)(.rβπ»)(πβ(π βf β π₯)))) |
45 | 44 | mpteq2dva 5209 |
. . . . . 6
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))) = (π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ»)(πβ(π βf β π₯))))) |
46 | 45 | oveq2d 7377 |
. . . . 5
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π» Ξ£g
(π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯))))) = (π» Ξ£g (π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ»)(πβ(π βf β π₯)))))) |
47 | 40, 46 | eqtrd 2773 |
. . . 4
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π
Ξ£g
(π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯))))) = (π» Ξ£g (π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ»)(πβ(π βf β π₯)))))) |
48 | 47 | mpteq2dva 5209 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ (π
Ξ£g
(π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))))) = (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ (π» Ξ£g
(π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ»)(πβ(π βf β π₯))))))) |
49 | | resspsr.s |
. . . 4
β’ π = (πΌ mPwSer π
) |
50 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
51 | | eqid 2733 |
. . . 4
β’
(.rβπ) = (.rβπ) |
52 | | fvex 6859 |
. . . . . . . 8
β’
(Baseβπ
)
β V |
53 | 4, 21 | syl 17 |
. . . . . . . . 9
β’ (π β π = (Baseβπ»)) |
54 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ
) =
(Baseβπ
) |
55 | 54 | subrgss 20265 |
. . . . . . . . . 10
β’ (π β (SubRingβπ
) β π β (Baseβπ
)) |
56 | 4, 55 | syl 17 |
. . . . . . . . 9
β’ (π β π β (Baseβπ
)) |
57 | 53, 56 | eqsstrrd 3987 |
. . . . . . . 8
β’ (π β (Baseβπ») β (Baseβπ
)) |
58 | | mapss 8833 |
. . . . . . . 8
β’
(((Baseβπ
)
β V β§ (Baseβπ») β (Baseβπ
)) β ((Baseβπ») βm {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
((Baseβπ
)
βm {π
β (β0 βm πΌ) β£ (β‘π β β) β
Fin})) |
59 | 52, 57, 58 | sylancr 588 |
. . . . . . 7
β’ (π β ((Baseβπ») βm {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
((Baseβπ
)
βm {π
β (β0 βm πΌ) β£ (β‘π β β) β
Fin})) |
60 | 59 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β ((Baseβπ») βm {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
((Baseβπ
)
βm {π
β (β0 βm πΌ) β£ (β‘π β β) β
Fin})) |
61 | | reldmpsr 21339 |
. . . . . . . . . 10
β’ Rel dom
mPwSer |
62 | 61, 11, 13 | elbasov 17098 |
. . . . . . . . 9
β’ (π β π΅ β (πΌ β V β§ π» β V)) |
63 | 62 | ad2antrl 727 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β (πΌ β V β§ π» β V)) |
64 | 63 | simpld 496 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅)) β πΌ β V) |
65 | 11, 12, 1, 13, 64 | psrbas 21369 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β π΅ = ((Baseβπ») βm {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin})) |
66 | 49, 54, 1, 50, 64 | psrbas 21369 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β (Baseβπ) = ((Baseβπ
) βm {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin})) |
67 | 60, 65, 66 | 3sstr4d 3995 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β π΅ β (Baseβπ)) |
68 | 67, 14 | sseldd 3949 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β (Baseβπ)) |
69 | 67, 24 | sseldd 3949 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β (Baseβπ)) |
70 | 49, 50, 36, 51, 1, 68, 69 | psrmulfval 21376 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(.rβπ)π) = (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ (π
Ξ£g
(π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯))))))) |
71 | | eqid 2733 |
. . . 4
β’
(.rβπ») = (.rβπ») |
72 | | eqid 2733 |
. . . 4
β’
(.rβπ) = (.rβπ) |
73 | 11, 13, 71, 72, 1, 14, 24 | psrmulfval 21376 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(.rβπ)π) = (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ (π» Ξ£g
(π₯ β {π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ»)(πβ(π βf β π₯))))))) |
74 | 48, 70, 73 | 3eqtr4rd 2784 |
. 2
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(.rβπ)π) = (π(.rβπ)π)) |
75 | 13 | fvexi 6860 |
. . . 4
β’ π΅ β V |
76 | | resspsr.p |
. . . . 5
β’ π = (π βΎs π΅) |
77 | 76, 51 | ressmulr 17196 |
. . . 4
β’ (π΅ β V β
(.rβπ) =
(.rβπ)) |
78 | 75, 77 | mp1i 13 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (.rβπ) = (.rβπ)) |
79 | 78 | oveqd 7378 |
. 2
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(.rβπ)π) = (π(.rβπ)π)) |
80 | 74, 79 | eqtrd 2773 |
1
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(.rβπ)π) = (π(.rβπ)π)) |