Step | Hyp | Ref
| Expression |
1 | | imasvscaf.u |
. . . . . . 7
β’ (π β π = (πΉ βs π
)) |
2 | | imasvscaf.v |
. . . . . . 7
β’ (π β π = (Baseβπ
)) |
3 | | imasvscaf.f |
. . . . . . 7
β’ (π β πΉ:πβontoβπ΅) |
4 | | imasvscaf.r |
. . . . . . 7
β’ (π β π
β π) |
5 | | imasvscaf.g |
. . . . . . 7
β’ πΊ = (Scalarβπ
) |
6 | | imasvscaf.k |
. . . . . . 7
β’ πΎ = (BaseβπΊ) |
7 | | imasvscaf.q |
. . . . . . 7
β’ Β· = (
Β·π βπ
) |
8 | | imasvscaf.s |
. . . . . . 7
β’ β = (
Β·π βπ) |
9 | | imasvscaf.e |
. . . . . . 7
β’ ((π β§ (π β πΎ β§ π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | imasvscafn 17379 |
. . . . . 6
β’ (π β β Fn (πΎ Γ π΅)) |
11 | | fnfun 6599 |
. . . . . 6
β’ ( β Fn
(πΎ Γ π΅) β Fun β ) |
12 | 10, 11 | syl 17 |
. . . . 5
β’ (π β Fun β ) |
13 | 12 | 3ad2ant1 1133 |
. . . 4
β’ ((π β§ π β πΎ β§ π β π) β Fun β ) |
14 | | eqidd 2738 |
. . . . . . . 8
β’ (π = π β πΎ = πΎ) |
15 | | fveq2 6839 |
. . . . . . . . 9
β’ (π = π β (πΉβπ) = (πΉβπ)) |
16 | 15 | sneqd 4596 |
. . . . . . . 8
β’ (π = π β {(πΉβπ)} = {(πΉβπ)}) |
17 | | oveq2 7359 |
. . . . . . . . 9
β’ (π = π β (π Β· π) = (π Β· π)) |
18 | 17 | fveq2d 6843 |
. . . . . . . 8
β’ (π = π β (πΉβ(π Β· π)) = (πΉβ(π Β· π))) |
19 | 14, 16, 18 | mpoeq123dv 7426 |
. . . . . . 7
β’ (π = π β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) = (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) |
20 | 19 | ssiun2s 5006 |
. . . . . 6
β’ (π β π β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) |
21 | 20 | 3ad2ant3 1135 |
. . . . 5
β’ ((π β§ π β πΎ β§ π β π) β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) |
22 | 1, 2, 3, 4, 5, 6, 7, 8 | imasvsca 17362 |
. . . . . 6
β’ (π β β = βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) |
23 | 22 | 3ad2ant1 1133 |
. . . . 5
β’ ((π β§ π β πΎ β§ π β π) β β = βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) |
24 | 21, 23 | sseqtrrd 3983 |
. . . 4
β’ ((π β§ π β πΎ β§ π β π) β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β β ) |
25 | | simp2 1137 |
. . . . . 6
β’ ((π β§ π β πΎ β§ π β π) β π β πΎ) |
26 | | fvex 6852 |
. . . . . . 7
β’ (πΉβπ) β V |
27 | 26 | snid 4620 |
. . . . . 6
β’ (πΉβπ) β {(πΉβπ)} |
28 | | opelxpi 5668 |
. . . . . 6
β’ ((π β πΎ β§ (πΉβπ) β {(πΉβπ)}) β β¨π, (πΉβπ)β© β (πΎ Γ {(πΉβπ)})) |
29 | 25, 27, 28 | sylancl 586 |
. . . . 5
β’ ((π β§ π β πΎ β§ π β π) β β¨π, (πΉβπ)β© β (πΎ Γ {(πΉβπ)})) |
30 | | eqid 2737 |
. . . . . 6
β’ (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) = (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) |
31 | | fvex 6852 |
. . . . . 6
β’ (πΉβ(π Β· π)) β V |
32 | 30, 31 | dmmpo 7995 |
. . . . 5
β’ dom
(π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) = (πΎ Γ {(πΉβπ)}) |
33 | 29, 32 | eleqtrrdi 2849 |
. . . 4
β’ ((π β§ π β πΎ β§ π β π) β β¨π, (πΉβπ)β© β dom (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) |
34 | | funssfv 6860 |
. . . 4
β’ ((Fun
β
β§ (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β β β§ β¨π, (πΉβπ)β© β dom (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) β ( β ββ¨π, (πΉβπ)β©) = ((π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))ββ¨π, (πΉβπ)β©)) |
35 | 13, 24, 33, 34 | syl3anc 1371 |
. . 3
β’ ((π β§ π β πΎ β§ π β π) β ( β ββ¨π, (πΉβπ)β©) = ((π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))ββ¨π, (πΉβπ)β©)) |
36 | | df-ov 7354 |
. . 3
β’ (π β (πΉβπ)) = ( β ββ¨π, (πΉβπ)β©) |
37 | | df-ov 7354 |
. . 3
β’ (π(π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))(πΉβπ)) = ((π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))ββ¨π, (πΉβπ)β©) |
38 | 35, 36, 37 | 3eqtr4g 2802 |
. 2
β’ ((π β§ π β πΎ β§ π β π) β (π β (πΉβπ)) = (π(π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))(πΉβπ))) |
39 | | fvoveq1 7374 |
. . . 4
β’ (π = π β (πΉβ(π Β· π)) = (πΉβ(π Β· π))) |
40 | | eqidd 2738 |
. . . 4
β’ (π₯ = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π))) |
41 | | fvex 6852 |
. . . 4
β’ (πΉβ(π Β· π)) β V |
42 | 39, 40, 30, 41 | ovmpo 7509 |
. . 3
β’ ((π β πΎ β§ (πΉβπ) β {(πΉβπ)}) β (π(π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))(πΉβπ)) = (πΉβ(π Β· π))) |
43 | 25, 27, 42 | sylancl 586 |
. 2
β’ ((π β§ π β πΎ β§ π β π) β (π(π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))(πΉβπ)) = (πΉβ(π Β· π))) |
44 | 38, 43 | eqtrd 2777 |
1
β’ ((π β§ π β πΎ β§ π β π) β (π β (πΉβπ)) = (πΉβ(π Β· π))) |