Step | Hyp | Ref
| Expression |
1 | | resspsr.u |
. . 3
β’ π = (πΌ mPwSer π») |
2 | | resspsr.b |
. . 3
β’ π΅ = (Baseβπ) |
3 | | eqid 2733 |
. . 3
β’
(+gβπ») = (+gβπ») |
4 | | eqid 2733 |
. . 3
β’
(+gβπ) = (+gβπ) |
5 | | simprl 770 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π΅) |
6 | | simprr 772 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π΅) |
7 | 1, 2, 3, 4, 5, 6 | psradd 21373 |
. 2
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(+gβπ)π) = (π βf
(+gβπ»)π)) |
8 | | resspsr.s |
. . . 4
β’ π = (πΌ mPwSer π
) |
9 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
10 | | eqid 2733 |
. . . 4
β’
(+gβπ
) = (+gβπ
) |
11 | | eqid 2733 |
. . . 4
β’
(+gβπ) = (+gβπ) |
12 | | fvex 6859 |
. . . . . . . 8
β’
(Baseβπ
)
β V |
13 | | resspsr.2 |
. . . . . . . . . 10
β’ (π β π β (SubRingβπ
)) |
14 | | resspsr.h |
. . . . . . . . . . 11
β’ π» = (π
βΎs π) |
15 | 14 | subrgbas 20273 |
. . . . . . . . . 10
β’ (π β (SubRingβπ
) β π = (Baseβπ»)) |
16 | 13, 15 | syl 17 |
. . . . . . . . 9
β’ (π β π = (Baseβπ»)) |
17 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ
) =
(Baseβπ
) |
18 | 17 | subrgss 20265 |
. . . . . . . . . 10
β’ (π β (SubRingβπ
) β π β (Baseβπ
)) |
19 | 13, 18 | syl 17 |
. . . . . . . . 9
β’ (π β π β (Baseβπ
)) |
20 | 16, 19 | eqsstrrd 3987 |
. . . . . . . 8
β’ (π β (Baseβπ») β (Baseβπ
)) |
21 | | mapss 8833 |
. . . . . . . 8
β’
(((Baseβπ
)
β V β§ (Baseβπ») β (Baseβπ
)) β ((Baseβπ») βm {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
((Baseβπ
)
βm {π
β (β0 βm πΌ) β£ (β‘π β β) β
Fin})) |
22 | 12, 20, 21 | sylancr 588 |
. . . . . . 7
β’ (π β ((Baseβπ») βm {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
((Baseβπ
)
βm {π
β (β0 βm πΌ) β£ (β‘π β β) β
Fin})) |
23 | 22 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β ((Baseβπ») βm {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
((Baseβπ
)
βm {π
β (β0 βm πΌ) β£ (β‘π β β) β
Fin})) |
24 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ») =
(Baseβπ») |
25 | | eqid 2733 |
. . . . . . 7
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
26 | | reldmpsr 21339 |
. . . . . . . . . 10
β’ Rel dom
mPwSer |
27 | 26, 1, 2 | elbasov 17098 |
. . . . . . . . 9
β’ (π β π΅ β (πΌ β V β§ π» β V)) |
28 | 27 | ad2antrl 727 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β (πΌ β V β§ π» β V)) |
29 | 28 | simpld 496 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅)) β πΌ β V) |
30 | 1, 24, 25, 2, 29 | psrbas 21369 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β π΅ = ((Baseβπ») βm {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin})) |
31 | 8, 17, 25, 9, 29 | psrbas 21369 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β (Baseβπ) = ((Baseβπ
) βm {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin})) |
32 | 23, 30, 31 | 3sstr4d 3995 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β π΅ β (Baseβπ)) |
33 | 32, 5 | sseldd 3949 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β (Baseβπ)) |
34 | 32, 6 | sseldd 3949 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β (Baseβπ)) |
35 | 8, 9, 10, 11, 33, 34 | psradd 21373 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(+gβπ)π) = (π βf
(+gβπ
)π)) |
36 | 14, 10 | ressplusg 17179 |
. . . . . . 7
β’ (π β (SubRingβπ
) β
(+gβπ
) =
(+gβπ»)) |
37 | 13, 36 | syl 17 |
. . . . . 6
β’ (π β (+gβπ
) = (+gβπ»)) |
38 | 37 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β (+gβπ
) = (+gβπ»)) |
39 | 38 | ofeqd 7623 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β βf
(+gβπ
) =
βf (+gβπ»)) |
40 | 39 | oveqd 7378 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π βf
(+gβπ
)π) = (π βf
(+gβπ»)π)) |
41 | 35, 40 | eqtrd 2773 |
. 2
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(+gβπ)π) = (π βf
(+gβπ»)π)) |
42 | 2 | fvexi 6860 |
. . . 4
β’ π΅ β V |
43 | | resspsr.p |
. . . . 5
β’ π = (π βΎs π΅) |
44 | 43, 11 | ressplusg 17179 |
. . . 4
β’ (π΅ β V β
(+gβπ) =
(+gβπ)) |
45 | 42, 44 | mp1i 13 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (+gβπ) = (+gβπ)) |
46 | 45 | oveqd 7378 |
. 2
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(+gβπ)π) = (π(+gβπ)π)) |
47 | 7, 41, 46 | 3eqtr2d 2779 |
1
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(+gβπ)π) = (π(+gβπ)π)) |