Step | Hyp | Ref
| Expression |
1 | | resspsr.u |
. . 3
β’ π = (πΌ mPwSer π») |
2 | | eqid 2733 |
. . 3
β’ (
Β·π βπ) = ( Β·π
βπ) |
3 | | eqid 2733 |
. . 3
β’
(Baseβπ») =
(Baseβπ») |
4 | | resspsr.b |
. . 3
β’ π΅ = (Baseβπ) |
5 | | eqid 2733 |
. . 3
β’
(.rβπ») = (.rβπ») |
6 | | eqid 2733 |
. . 3
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
7 | | simprl 770 |
. . . 4
β’ ((π β§ (π β π β§ π β π΅)) β π β π) |
8 | | resspsr.2 |
. . . . . 6
β’ (π β π β (SubRingβπ
)) |
9 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π β§ π β π΅)) β π β (SubRingβπ
)) |
10 | | resspsr.h |
. . . . . 6
β’ π» = (π
βΎs π) |
11 | 10 | subrgbas 20273 |
. . . . 5
β’ (π β (SubRingβπ
) β π = (Baseβπ»)) |
12 | 9, 11 | syl 17 |
. . . 4
β’ ((π β§ (π β π β§ π β π΅)) β π = (Baseβπ»)) |
13 | 7, 12 | eleqtrd 2836 |
. . 3
β’ ((π β§ (π β π β§ π β π΅)) β π β (Baseβπ»)) |
14 | | simprr 772 |
. . 3
β’ ((π β§ (π β π β§ π β π΅)) β π β π΅) |
15 | 1, 2, 3, 4, 5, 6, 13, 14 | psrvsca 21382 |
. 2
β’ ((π β§ (π β π β§ π β π΅)) β (π( Β·π
βπ)π) = (({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} Γ {π}) βf
(.rβπ»)π)) |
16 | | resspsr.s |
. . . 4
β’ π = (πΌ mPwSer π
) |
17 | | eqid 2733 |
. . . 4
β’ (
Β·π βπ) = ( Β·π
βπ) |
18 | | eqid 2733 |
. . . 4
β’
(Baseβπ
) =
(Baseβπ
) |
19 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
20 | | eqid 2733 |
. . . 4
β’
(.rβπ
) = (.rβπ
) |
21 | 18 | subrgss 20265 |
. . . . . 6
β’ (π β (SubRingβπ
) β π β (Baseβπ
)) |
22 | 9, 21 | syl 17 |
. . . . 5
β’ ((π β§ (π β π β§ π β π΅)) β π β (Baseβπ
)) |
23 | 22, 7 | sseldd 3949 |
. . . 4
β’ ((π β§ (π β π β§ π β π΅)) β π β (Baseβπ
)) |
24 | | resspsr.p |
. . . . . . . 8
β’ π = (π βΎs π΅) |
25 | 16, 10, 1, 4, 24, 8 | resspsrbas 21407 |
. . . . . . 7
β’ (π β π΅ = (Baseβπ)) |
26 | 24, 19 | ressbasss 17129 |
. . . . . . 7
β’
(Baseβπ)
β (Baseβπ) |
27 | 25, 26 | eqsstrdi 4002 |
. . . . . 6
β’ (π β π΅ β (Baseβπ)) |
28 | 27 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π β§ π β π΅)) β π΅ β (Baseβπ)) |
29 | 28, 14 | sseldd 3949 |
. . . 4
β’ ((π β§ (π β π β§ π β π΅)) β π β (Baseβπ)) |
30 | 16, 17, 18, 19, 20, 6, 23, 29 | psrvsca 21382 |
. . 3
β’ ((π β§ (π β π β§ π β π΅)) β (π( Β·π
βπ)π) = (({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} Γ {π}) βf
(.rβπ
)π)) |
31 | 10, 20 | ressmulr 17196 |
. . . . 5
β’ (π β (SubRingβπ
) β
(.rβπ
) =
(.rβπ»)) |
32 | | ofeq 7624 |
. . . . 5
β’
((.rβπ
) = (.rβπ») β βf
(.rβπ
) =
βf (.rβπ»)) |
33 | 9, 31, 32 | 3syl 18 |
. . . 4
β’ ((π β§ (π β π β§ π β π΅)) β βf
(.rβπ
) =
βf (.rβπ»)) |
34 | 33 | oveqd 7378 |
. . 3
β’ ((π β§ (π β π β§ π β π΅)) β (({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} Γ {π}) βf
(.rβπ
)π) = (({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} Γ {π}) βf
(.rβπ»)π)) |
35 | 30, 34 | eqtrd 2773 |
. 2
β’ ((π β§ (π β π β§ π β π΅)) β (π( Β·π
βπ)π) = (({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} Γ {π}) βf
(.rβπ»)π)) |
36 | 4 | fvexi 6860 |
. . . 4
β’ π΅ β V |
37 | 24, 17 | ressvsca 17233 |
. . . 4
β’ (π΅ β V β (
Β·π βπ) = ( Β·π
βπ)) |
38 | 36, 37 | mp1i 13 |
. . 3
β’ ((π β§ (π β π β§ π β π΅)) β (
Β·π βπ) = ( Β·π
βπ)) |
39 | 38 | oveqd 7378 |
. 2
β’ ((π β§ (π β π β§ π β π΅)) β (π( Β·π
βπ)π) = (π( Β·π
βπ)π)) |
40 | 15, 35, 39 | 3eqtr2d 2779 |
1
β’ ((π β§ (π β π β§ π β π΅)) β (π( Β·π
βπ)π) = (π( Β·π
βπ)π)) |