Step | Hyp | Ref
| Expression |
1 | | imasvscaf.u |
. . 3
β’ (π β π = (πΉ βs π
)) |
2 | | imasvscaf.v |
. . 3
β’ (π β π = (Baseβπ
)) |
3 | | imasvscaf.f |
. . 3
β’ (π β πΉ:πβontoβπ΅) |
4 | | imasvscaf.r |
. . 3
β’ (π β π
β π) |
5 | | imasvscaf.g |
. . 3
β’ πΊ = (Scalarβπ
) |
6 | | imasvscaf.k |
. . 3
β’ πΎ = (BaseβπΊ) |
7 | | imasvscaf.q |
. . 3
β’ Β· = (
Β·π βπ
) |
8 | | imasvscaf.s |
. . 3
β’ β = (
Β·π βπ) |
9 | | imasvscaf.e |
. . 3
β’ ((π β§ (π β πΎ β§ π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | imasvscafn 17420 |
. 2
β’ (π β β Fn (πΎ Γ π΅)) |
11 | 1, 2, 3, 4, 5, 6, 7, 8 | imasvsca 17403 |
. . 3
β’ (π β β = βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) |
12 | | imasvscaf.c |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΎ β§ π β π)) β (π Β· π) β π) |
13 | | fof 6757 |
. . . . . . . . . . . . . 14
β’ (πΉ:πβontoβπ΅ β πΉ:πβΆπ΅) |
14 | 3, 13 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β πΉ:πβΆπ΅) |
15 | 14 | ffvelcdmda 7036 |
. . . . . . . . . . . 12
β’ ((π β§ (π Β· π) β π) β (πΉβ(π Β· π)) β π΅) |
16 | 12, 15 | syldan 592 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΎ β§ π β π)) β (πΉβ(π Β· π)) β π΅) |
17 | 16 | ralrimivw 3148 |
. . . . . . . . . 10
β’ ((π β§ (π β πΎ β§ π β π)) β βπ₯ β {(πΉβπ)} (πΉβ(π Β· π)) β π΅) |
18 | 17 | anass1rs 654 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β πΎ) β βπ₯ β {(πΉβπ)} (πΉβ(π Β· π)) β π΅) |
19 | 18 | ralrimiva 3144 |
. . . . . . . 8
β’ ((π β§ π β π) β βπ β πΎ βπ₯ β {(πΉβπ)} (πΉβ(π Β· π)) β π΅) |
20 | | eqid 2737 |
. . . . . . . . 9
β’ (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) = (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) |
21 | 20 | fmpo 8001 |
. . . . . . . 8
β’
(βπ β
πΎ βπ₯ β {(πΉβπ)} (πΉβ(π Β· π)) β π΅ β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))):(πΎ Γ {(πΉβπ)})βΆπ΅) |
22 | 19, 21 | sylib 217 |
. . . . . . 7
β’ ((π β§ π β π) β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))):(πΎ Γ {(πΉβπ)})βΆπ΅) |
23 | | fssxp 6697 |
. . . . . . 7
β’ ((π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))):(πΎ Γ {(πΉβπ)})βΆπ΅ β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((πΎ Γ {(πΉβπ)}) Γ π΅)) |
24 | 22, 23 | syl 17 |
. . . . . 6
β’ ((π β§ π β π) β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((πΎ Γ {(πΉβπ)}) Γ π΅)) |
25 | 14 | ffvelcdmda 7036 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΉβπ) β π΅) |
26 | 25 | snssd 4770 |
. . . . . . 7
β’ ((π β§ π β π) β {(πΉβπ)} β π΅) |
27 | | xpss2 5654 |
. . . . . . 7
β’ ({(πΉβπ)} β π΅ β (πΎ Γ {(πΉβπ)}) β (πΎ Γ π΅)) |
28 | | xpss1 5653 |
. . . . . . 7
β’ ((πΎ Γ {(πΉβπ)}) β (πΎ Γ π΅) β ((πΎ Γ {(πΉβπ)}) Γ π΅) β ((πΎ Γ π΅) Γ π΅)) |
29 | 26, 27, 28 | 3syl 18 |
. . . . . 6
β’ ((π β§ π β π) β ((πΎ Γ {(πΉβπ)}) Γ π΅) β ((πΎ Γ π΅) Γ π΅)) |
30 | 24, 29 | sstrd 3955 |
. . . . 5
β’ ((π β§ π β π) β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((πΎ Γ π΅) Γ π΅)) |
31 | 30 | ralrimiva 3144 |
. . . 4
β’ (π β βπ β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((πΎ Γ π΅) Γ π΅)) |
32 | | iunss 5006 |
. . . 4
β’ (βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((πΎ Γ π΅) Γ π΅) β βπ β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((πΎ Γ π΅) Γ π΅)) |
33 | 31, 32 | sylibr 233 |
. . 3
β’ (π β βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((πΎ Γ π΅) Γ π΅)) |
34 | 11, 33 | eqsstrd 3983 |
. 2
β’ (π β β β ((πΎ Γ π΅) Γ π΅)) |
35 | | dff2 7050 |
. 2
β’ ( β
:(πΎ Γ π΅)βΆπ΅ β ( β Fn (πΎ Γ π΅) β§ β β ((πΎ Γ π΅) Γ π΅))) |
36 | 10, 34, 35 | sylanbrc 584 |
1
β’ (π β β :(πΎ Γ π΅)βΆπ΅) |