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