Step | Hyp | Ref
| Expression |
1 | | lkrsc.v |
. . . . . . . . 9
β’ π = (Baseβπ) |
2 | 1 | fvexi 6860 |
. . . . . . . 8
β’ π β V |
3 | 2 | a1i 11 |
. . . . . . 7
β’ (π β π β V) |
4 | | lkrsc.r |
. . . . . . 7
β’ (π β π
β πΎ) |
5 | | lkrsc.w |
. . . . . . . . 9
β’ (π β π β LVec) |
6 | | lkrsc.g |
. . . . . . . . 9
β’ (π β πΊ β πΉ) |
7 | | lkrsc.d |
. . . . . . . . . 10
β’ π· = (Scalarβπ) |
8 | | lkrsc.k |
. . . . . . . . . 10
β’ πΎ = (Baseβπ·) |
9 | | lkrsc.f |
. . . . . . . . . 10
β’ πΉ = (LFnlβπ) |
10 | 7, 8, 1, 9 | lflf 37575 |
. . . . . . . . 9
β’ ((π β LVec β§ πΊ β πΉ) β πΊ:πβΆπΎ) |
11 | 5, 6, 10 | syl2anc 585 |
. . . . . . . 8
β’ (π β πΊ:πβΆπΎ) |
12 | 11 | ffnd 6673 |
. . . . . . 7
β’ (π β πΊ Fn π) |
13 | | eqidd 2734 |
. . . . . . 7
β’ ((π β§ π£ β π) β (πΊβπ£) = (πΊβπ£)) |
14 | 3, 4, 12, 13 | ofc2 7648 |
. . . . . 6
β’ ((π β§ π£ β π) β ((πΊ βf Β· (π Γ {π
}))βπ£) = ((πΊβπ£) Β· π
)) |
15 | 14 | eqeq1d 2735 |
. . . . 5
β’ ((π β§ π£ β π) β (((πΊ βf Β· (π Γ {π
}))βπ£) = 0 β ((πΊβπ£) Β· π
) = 0 )) |
16 | | lkrsc.o |
. . . . . 6
β’ 0 =
(0gβπ·) |
17 | | lkrsc.t |
. . . . . 6
β’ Β· =
(.rβπ·) |
18 | 7 | lvecdrng 20610 |
. . . . . . . 8
β’ (π β LVec β π· β
DivRing) |
19 | 5, 18 | syl 17 |
. . . . . . 7
β’ (π β π· β DivRing) |
20 | 19 | adantr 482 |
. . . . . 6
β’ ((π β§ π£ β π) β π· β DivRing) |
21 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ π£ β π) β π β LVec) |
22 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ π£ β π) β πΊ β πΉ) |
23 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π£ β π) β π£ β π) |
24 | 7, 8, 1, 9 | lflcl 37576 |
. . . . . . 7
β’ ((π β LVec β§ πΊ β πΉ β§ π£ β π) β (πΊβπ£) β πΎ) |
25 | 21, 22, 23, 24 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π£ β π) β (πΊβπ£) β πΎ) |
26 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ π£ β π) β π
β πΎ) |
27 | | lkrsc.e |
. . . . . . 7
β’ (π β π
β 0 ) |
28 | 27 | adantr 482 |
. . . . . 6
β’ ((π β§ π£ β π) β π
β 0 ) |
29 | 8, 16, 17, 20, 25, 26, 28 | drngmuleq0 20247 |
. . . . 5
β’ ((π β§ π£ β π) β (((πΊβπ£) Β· π
) = 0 β (πΊβπ£) = 0 )) |
30 | 15, 29 | bitrd 279 |
. . . 4
β’ ((π β§ π£ β π) β (((πΊ βf Β· (π Γ {π
}))βπ£) = 0 β (πΊβπ£) = 0 )) |
31 | 30 | pm5.32da 580 |
. . 3
β’ (π β ((π£ β π β§ ((πΊ βf Β· (π Γ {π
}))βπ£) = 0 ) β (π£ β π β§ (πΊβπ£) = 0 ))) |
32 | | lveclmod 20611 |
. . . . . 6
β’ (π β LVec β π β LMod) |
33 | 5, 32 | syl 17 |
. . . . 5
β’ (π β π β LMod) |
34 | 1, 7, 8, 17, 9, 33, 6, 4 | lflvscl 37589 |
. . . 4
β’ (π β (πΊ βf Β· (π Γ {π
})) β πΉ) |
35 | | lkrsc.l |
. . . . 5
β’ πΏ = (LKerβπ) |
36 | 1, 7, 16, 9, 35 | ellkr 37601 |
. . . 4
β’ ((π β LVec β§ (πΊ βf Β· (π Γ {π
})) β πΉ) β (π£ β (πΏβ(πΊ βf Β· (π Γ {π
}))) β (π£ β π β§ ((πΊ βf Β· (π Γ {π
}))βπ£) = 0 ))) |
37 | 5, 34, 36 | syl2anc 585 |
. . 3
β’ (π β (π£ β (πΏβ(πΊ βf Β· (π Γ {π
}))) β (π£ β π β§ ((πΊ βf Β· (π Γ {π
}))βπ£) = 0 ))) |
38 | 1, 7, 16, 9, 35 | ellkr 37601 |
. . . 4
β’ ((π β LVec β§ πΊ β πΉ) β (π£ β (πΏβπΊ) β (π£ β π β§ (πΊβπ£) = 0 ))) |
39 | 5, 6, 38 | syl2anc 585 |
. . 3
β’ (π β (π£ β (πΏβπΊ) β (π£ β π β§ (πΊβπ£) = 0 ))) |
40 | 31, 37, 39 | 3bitr4d 311 |
. 2
β’ (π β (π£ β (πΏβ(πΊ βf Β· (π Γ {π
}))) β π£ β (πΏβπΊ))) |
41 | 40 | eqrdv 2731 |
1
β’ (π β (πΏβ(πΊ βf Β· (π Γ {π
}))) = (πΏβπΊ)) |