Step | Hyp | Ref
| Expression |
1 | | eqlkr.d |
. . 3
β’ π· = (Scalarβπ) |
2 | | eqlkr.k |
. . 3
β’ πΎ = (Baseβπ·) |
3 | | eqlkr.t |
. . 3
β’ Β· =
(.rβπ·) |
4 | | eqlkr.v |
. . 3
β’ π = (Baseβπ) |
5 | | eqlkr.f |
. . 3
β’ πΉ = (LFnlβπ) |
6 | | eqlkr.l |
. . 3
β’ πΏ = (LKerβπ) |
7 | 1, 2, 3, 4, 5, 6 | eqlkr 37611 |
. 2
β’ ((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β βπ β πΎ βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· π)) |
8 | 4 | fvexi 6860 |
. . . . 5
β’ π β V |
9 | 8 | a1i 11 |
. . . 4
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ π β πΎ) β π β V) |
10 | | simpl1 1192 |
. . . . . 6
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ π β πΎ) β π β LVec) |
11 | | simpl2l 1227 |
. . . . . 6
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ π β πΎ) β πΊ β πΉ) |
12 | 1, 2, 4, 5 | lflf 37575 |
. . . . . 6
β’ ((π β LVec β§ πΊ β πΉ) β πΊ:πβΆπΎ) |
13 | 10, 11, 12 | syl2anc 585 |
. . . . 5
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ π β πΎ) β πΊ:πβΆπΎ) |
14 | 13 | ffnd 6673 |
. . . 4
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ π β πΎ) β πΊ Fn π) |
15 | | vex 3451 |
. . . . 5
β’ π β V |
16 | | fnconstg 6734 |
. . . . 5
β’ (π β V β (π Γ {π}) Fn π) |
17 | 15, 16 | mp1i 13 |
. . . 4
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ π β πΎ) β (π Γ {π}) Fn π) |
18 | | simpl2r 1228 |
. . . . . 6
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ π β πΎ) β π» β πΉ) |
19 | 1, 2, 4, 5 | lflf 37575 |
. . . . . 6
β’ ((π β LVec β§ π» β πΉ) β π»:πβΆπΎ) |
20 | 10, 18, 19 | syl2anc 585 |
. . . . 5
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ π β πΎ) β π»:πβΆπΎ) |
21 | 20 | ffnd 6673 |
. . . 4
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ π β πΎ) β π» Fn π) |
22 | | eqidd 2734 |
. . . 4
β’ ((((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ π β πΎ) β§ π₯ β π) β (πΊβπ₯) = (πΊβπ₯)) |
23 | 15 | fvconst2 7157 |
. . . . 5
β’ (π₯ β π β ((π Γ {π})βπ₯) = π) |
24 | 23 | adantl 483 |
. . . 4
β’ ((((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ π β πΎ) β§ π₯ β π) β ((π Γ {π})βπ₯) = π) |
25 | 9, 14, 17, 21, 22, 24 | offveqb 7646 |
. . 3
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ π β πΎ) β (π» = (πΊ βf Β· (π Γ {π})) β βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· π))) |
26 | 25 | rexbidva 3170 |
. 2
β’ ((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β (βπ β πΎ π» = (πΊ βf Β· (π Γ {π})) β βπ β πΎ βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· π))) |
27 | 7, 26 | mpbird 257 |
1
β’ ((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β βπ β πΎ π» = (πΊ βf Β· (π Γ {π}))) |