Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
β’
((Scalarβπ
)Xs(πΌ Γ {π
})) = ((Scalarβπ
)Xs(πΌ Γ {π
})) |
2 | | eqid 2737 |
. . . 4
β’
(Baseβ((Scalarβπ
)Xs(πΌ Γ {π
}))) = (Baseβ((Scalarβπ
)Xs(πΌ Γ {π
}))) |
3 | | fvexd 6858 |
. . . 4
β’ (π β (Scalarβπ
) β V) |
4 | | pwsplusgval.i |
. . . 4
β’ (π β πΌ β π) |
5 | | pwsplusgval.r |
. . . . 5
β’ (π β π
β π) |
6 | | fnconstg 6731 |
. . . . 5
β’ (π
β π β (πΌ Γ {π
}) Fn πΌ) |
7 | 5, 6 | syl 17 |
. . . 4
β’ (π β (πΌ Γ {π
}) Fn πΌ) |
8 | | pwsplusgval.f |
. . . . 5
β’ (π β πΉ β π΅) |
9 | | pwsplusgval.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
10 | | pwsplusgval.y |
. . . . . . . . 9
β’ π = (π
βs πΌ) |
11 | | eqid 2737 |
. . . . . . . . 9
β’
(Scalarβπ
) =
(Scalarβπ
) |
12 | 10, 11 | pwsval 17369 |
. . . . . . . 8
β’ ((π
β π β§ πΌ β π) β π = ((Scalarβπ
)Xs(πΌ Γ {π
}))) |
13 | 5, 4, 12 | syl2anc 585 |
. . . . . . 7
β’ (π β π = ((Scalarβπ
)Xs(πΌ Γ {π
}))) |
14 | 13 | fveq2d 6847 |
. . . . . 6
β’ (π β (Baseβπ) =
(Baseβ((Scalarβπ
)Xs(πΌ Γ {π
})))) |
15 | 9, 14 | eqtrid 2789 |
. . . . 5
β’ (π β π΅ = (Baseβ((Scalarβπ
)Xs(πΌ Γ {π
})))) |
16 | 8, 15 | eleqtrd 2840 |
. . . 4
β’ (π β πΉ β (Baseβ((Scalarβπ
)Xs(πΌ Γ {π
})))) |
17 | | pwsplusgval.g |
. . . . 5
β’ (π β πΊ β π΅) |
18 | 17, 15 | eleqtrd 2840 |
. . . 4
β’ (π β πΊ β (Baseβ((Scalarβπ
)Xs(πΌ Γ {π
})))) |
19 | | eqid 2737 |
. . . 4
β’
(.rβ((Scalarβπ
)Xs(πΌ Γ {π
}))) =
(.rβ((Scalarβπ
)Xs(πΌ Γ {π
}))) |
20 | 1, 2, 3, 4, 7, 16,
18, 19 | prdsmulrval 17358 |
. . 3
β’ (π β (πΉ(.rβ((Scalarβπ
)Xs(πΌ Γ {π
})))πΊ) = (π₯ β πΌ β¦ ((πΉβπ₯)(.rβ((πΌ Γ {π
})βπ₯))(πΊβπ₯)))) |
21 | | fvconst2g 7152 |
. . . . . . . 8
β’ ((π
β π β§ π₯ β πΌ) β ((πΌ Γ {π
})βπ₯) = π
) |
22 | 5, 21 | sylan 581 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β ((πΌ Γ {π
})βπ₯) = π
) |
23 | 22 | fveq2d 6847 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β (.rβ((πΌ Γ {π
})βπ₯)) = (.rβπ
)) |
24 | | pwsmulrval.a |
. . . . . 6
β’ Β· =
(.rβπ
) |
25 | 23, 24 | eqtr4di 2795 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β (.rβ((πΌ Γ {π
})βπ₯)) = Β· ) |
26 | 25 | oveqd 7375 |
. . . 4
β’ ((π β§ π₯ β πΌ) β ((πΉβπ₯)(.rβ((πΌ Γ {π
})βπ₯))(πΊβπ₯)) = ((πΉβπ₯) Β· (πΊβπ₯))) |
27 | 26 | mpteq2dva 5206 |
. . 3
β’ (π β (π₯ β πΌ β¦ ((πΉβπ₯)(.rβ((πΌ Γ {π
})βπ₯))(πΊβπ₯))) = (π₯ β πΌ β¦ ((πΉβπ₯) Β· (πΊβπ₯)))) |
28 | 20, 27 | eqtrd 2777 |
. 2
β’ (π β (πΉ(.rβ((Scalarβπ
)Xs(πΌ Γ {π
})))πΊ) = (π₯ β πΌ β¦ ((πΉβπ₯) Β· (πΊβπ₯)))) |
29 | | pwsmulrval.p |
. . . 4
β’ β =
(.rβπ) |
30 | 13 | fveq2d 6847 |
. . . 4
β’ (π β (.rβπ) =
(.rβ((Scalarβπ
)Xs(πΌ Γ {π
})))) |
31 | 29, 30 | eqtrid 2789 |
. . 3
β’ (π β β =
(.rβ((Scalarβπ
)Xs(πΌ Γ {π
})))) |
32 | 31 | oveqd 7375 |
. 2
β’ (π β (πΉ β πΊ) = (πΉ(.rβ((Scalarβπ
)Xs(πΌ Γ {π
})))πΊ)) |
33 | | fvexd 6858 |
. . 3
β’ ((π β§ π₯ β πΌ) β (πΉβπ₯) β V) |
34 | | fvexd 6858 |
. . 3
β’ ((π β§ π₯ β πΌ) β (πΊβπ₯) β V) |
35 | | eqid 2737 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ
) |
36 | 10, 35, 9, 5, 4, 8 | pwselbas 17372 |
. . . 4
β’ (π β πΉ:πΌβΆ(Baseβπ
)) |
37 | 36 | feqmptd 6911 |
. . 3
β’ (π β πΉ = (π₯ β πΌ β¦ (πΉβπ₯))) |
38 | 10, 35, 9, 5, 4, 17 | pwselbas 17372 |
. . . 4
β’ (π β πΊ:πΌβΆ(Baseβπ
)) |
39 | 38 | feqmptd 6911 |
. . 3
β’ (π β πΊ = (π₯ β πΌ β¦ (πΊβπ₯))) |
40 | 4, 33, 34, 37, 39 | offval2 7638 |
. 2
β’ (π β (πΉ βf Β· πΊ) = (π₯ β πΌ β¦ ((πΉβπ₯) Β· (πΊβπ₯)))) |
41 | 28, 32, 40 | 3eqtr4d 2787 |
1
β’ (π β (πΉ β πΊ) = (πΉ βf Β· πΊ)) |