Step | Hyp | Ref
| Expression |
1 | | lmhmlsp.v |
. . . . . 6
β’ π = (Baseβπ) |
2 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
3 | 1, 2 | lmhmf 20510 |
. . . . 5
β’ (πΉ β (π LMHom π) β πΉ:πβΆ(Baseβπ)) |
4 | 3 | adantr 482 |
. . . 4
β’ ((πΉ β (π LMHom π) β§ π β π) β πΉ:πβΆ(Baseβπ)) |
5 | 4 | ffund 6673 |
. . 3
β’ ((πΉ β (π LMHom π) β§ π β π) β Fun πΉ) |
6 | | lmhmlmod1 20509 |
. . . . 5
β’ (πΉ β (π LMHom π) β π β LMod) |
7 | 6 | adantr 482 |
. . . 4
β’ ((πΉ β (π LMHom π) β§ π β π) β π β LMod) |
8 | | lmhmlmod2 20508 |
. . . . . . 7
β’ (πΉ β (π LMHom π) β π β LMod) |
9 | 8 | adantr 482 |
. . . . . 6
β’ ((πΉ β (π LMHom π) β§ π β π) β π β LMod) |
10 | | imassrn 6025 |
. . . . . . 7
β’ (πΉ β π) β ran πΉ |
11 | 4 | frnd 6677 |
. . . . . . 7
β’ ((πΉ β (π LMHom π) β§ π β π) β ran πΉ β (Baseβπ)) |
12 | 10, 11 | sstrid 3956 |
. . . . . 6
β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ β π) β (Baseβπ)) |
13 | | eqid 2733 |
. . . . . . 7
β’
(LSubSpβπ) =
(LSubSpβπ) |
14 | | lmhmlsp.l |
. . . . . . 7
β’ πΏ = (LSpanβπ) |
15 | 2, 13, 14 | lspcl 20452 |
. . . . . 6
β’ ((π β LMod β§ (πΉ β π) β (Baseβπ)) β (πΏβ(πΉ β π)) β (LSubSpβπ)) |
16 | 9, 12, 15 | syl2anc 585 |
. . . . 5
β’ ((πΉ β (π LMHom π) β§ π β π) β (πΏβ(πΉ β π)) β (LSubSpβπ)) |
17 | | eqid 2733 |
. . . . . 6
β’
(LSubSpβπ) =
(LSubSpβπ) |
18 | 17, 13 | lmhmpreima 20524 |
. . . . 5
β’ ((πΉ β (π LMHom π) β§ (πΏβ(πΉ β π)) β (LSubSpβπ)) β (β‘πΉ β (πΏβ(πΉ β π))) β (LSubSpβπ)) |
19 | 16, 18 | syldan 592 |
. . . 4
β’ ((πΉ β (π LMHom π) β§ π β π) β (β‘πΉ β (πΏβ(πΉ β π))) β (LSubSpβπ)) |
20 | | incom 4162 |
. . . . . . 7
β’ (dom
πΉ β© π) = (π β© dom πΉ) |
21 | | simpr 486 |
. . . . . . . . 9
β’ ((πΉ β (π LMHom π) β§ π β π) β π β π) |
22 | 4 | fdmd 6680 |
. . . . . . . . 9
β’ ((πΉ β (π LMHom π) β§ π β π) β dom πΉ = π) |
23 | 21, 22 | sseqtrrd 3986 |
. . . . . . . 8
β’ ((πΉ β (π LMHom π) β§ π β π) β π β dom πΉ) |
24 | | df-ss 3928 |
. . . . . . . 8
β’ (π β dom πΉ β (π β© dom πΉ) = π) |
25 | 23, 24 | sylib 217 |
. . . . . . 7
β’ ((πΉ β (π LMHom π) β§ π β π) β (π β© dom πΉ) = π) |
26 | 20, 25 | eqtr2id 2786 |
. . . . . 6
β’ ((πΉ β (π LMHom π) β§ π β π) β π = (dom πΉ β© π)) |
27 | | dminss 6106 |
. . . . . 6
β’ (dom
πΉ β© π) β (β‘πΉ β (πΉ β π)) |
28 | 26, 27 | eqsstrdi 3999 |
. . . . 5
β’ ((πΉ β (π LMHom π) β§ π β π) β π β (β‘πΉ β (πΉ β π))) |
29 | 2, 14 | lspssid 20461 |
. . . . . . 7
β’ ((π β LMod β§ (πΉ β π) β (Baseβπ)) β (πΉ β π) β (πΏβ(πΉ β π))) |
30 | 9, 12, 29 | syl2anc 585 |
. . . . . 6
β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ β π) β (πΏβ(πΉ β π))) |
31 | | imass2 6055 |
. . . . . 6
β’ ((πΉ β π) β (πΏβ(πΉ β π)) β (β‘πΉ β (πΉ β π)) β (β‘πΉ β (πΏβ(πΉ β π)))) |
32 | 30, 31 | syl 17 |
. . . . 5
β’ ((πΉ β (π LMHom π) β§ π β π) β (β‘πΉ β (πΉ β π)) β (β‘πΉ β (πΏβ(πΉ β π)))) |
33 | 28, 32 | sstrd 3955 |
. . . 4
β’ ((πΉ β (π LMHom π) β§ π β π) β π β (β‘πΉ β (πΏβ(πΉ β π)))) |
34 | | lmhmlsp.k |
. . . . 5
β’ πΎ = (LSpanβπ) |
35 | 17, 34 | lspssp 20464 |
. . . 4
β’ ((π β LMod β§ (β‘πΉ β (πΏβ(πΉ β π))) β (LSubSpβπ) β§ π β (β‘πΉ β (πΏβ(πΉ β π)))) β (πΎβπ) β (β‘πΉ β (πΏβ(πΉ β π)))) |
36 | 7, 19, 33, 35 | syl3anc 1372 |
. . 3
β’ ((πΉ β (π LMHom π) β§ π β π) β (πΎβπ) β (β‘πΉ β (πΏβ(πΉ β π)))) |
37 | | funimass2 6585 |
. . 3
β’ ((Fun
πΉ β§ (πΎβπ) β (β‘πΉ β (πΏβ(πΉ β π)))) β (πΉ β (πΎβπ)) β (πΏβ(πΉ β π))) |
38 | 5, 36, 37 | syl2anc 585 |
. 2
β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ β (πΎβπ)) β (πΏβ(πΉ β π))) |
39 | 1, 17, 34 | lspcl 20452 |
. . . . 5
β’ ((π β LMod β§ π β π) β (πΎβπ) β (LSubSpβπ)) |
40 | 7, 21, 39 | syl2anc 585 |
. . . 4
β’ ((πΉ β (π LMHom π) β§ π β π) β (πΎβπ) β (LSubSpβπ)) |
41 | 17, 13 | lmhmima 20523 |
. . . 4
β’ ((πΉ β (π LMHom π) β§ (πΎβπ) β (LSubSpβπ)) β (πΉ β (πΎβπ)) β (LSubSpβπ)) |
42 | 40, 41 | syldan 592 |
. . 3
β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ β (πΎβπ)) β (LSubSpβπ)) |
43 | 1, 34 | lspssid 20461 |
. . . . 5
β’ ((π β LMod β§ π β π) β π β (πΎβπ)) |
44 | 7, 21, 43 | syl2anc 585 |
. . . 4
β’ ((πΉ β (π LMHom π) β§ π β π) β π β (πΎβπ)) |
45 | | imass2 6055 |
. . . 4
β’ (π β (πΎβπ) β (πΉ β π) β (πΉ β (πΎβπ))) |
46 | 44, 45 | syl 17 |
. . 3
β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ β π) β (πΉ β (πΎβπ))) |
47 | 13, 14 | lspssp 20464 |
. . 3
β’ ((π β LMod β§ (πΉ β (πΎβπ)) β (LSubSpβπ) β§ (πΉ β π) β (πΉ β (πΎβπ))) β (πΏβ(πΉ β π)) β (πΉ β (πΎβπ))) |
48 | 9, 42, 46, 47 | syl3anc 1372 |
. 2
β’ ((πΉ β (π LMHom π) β§ π β π) β (πΏβ(πΉ β π)) β (πΉ β (πΎβπ))) |
49 | 38, 48 | eqssd 3962 |
1
β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ β (πΎβπ)) = (πΏβ(πΉ β π))) |