Proof of Theorem lmhmlsp
Step | Hyp | Ref
| Expression |
1 | | lmhmlsp.v |
. . . . . 6
⊢ 𝑉 = (Base‘𝑆) |
2 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑇) =
(Base‘𝑇) |
3 | 1, 2 | lmhmf 20071 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝑉⟶(Base‘𝑇)) |
4 | 3 | adantr 484 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝐹:𝑉⟶(Base‘𝑇)) |
5 | 4 | ffund 6549 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → Fun 𝐹) |
6 | | lmhmlmod1 20070 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) |
7 | 6 | adantr 484 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑆 ∈ LMod) |
8 | | lmhmlmod2 20069 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) |
9 | 8 | adantr 484 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑇 ∈ LMod) |
10 | | imassrn 5940 |
. . . . . . 7
⊢ (𝐹 “ 𝑈) ⊆ ran 𝐹 |
11 | 4 | frnd 6553 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → ran 𝐹 ⊆ (Base‘𝑇)) |
12 | 10, 11 | sstrid 3912 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ 𝑈) ⊆ (Base‘𝑇)) |
13 | | eqid 2737 |
. . . . . . 7
⊢
(LSubSp‘𝑇) =
(LSubSp‘𝑇) |
14 | | lmhmlsp.l |
. . . . . . 7
⊢ 𝐿 = (LSpan‘𝑇) |
15 | 2, 13, 14 | lspcl 20013 |
. . . . . 6
⊢ ((𝑇 ∈ LMod ∧ (𝐹 “ 𝑈) ⊆ (Base‘𝑇)) → (𝐿‘(𝐹 “ 𝑈)) ∈ (LSubSp‘𝑇)) |
16 | 9, 12, 15 | syl2anc 587 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐿‘(𝐹 “ 𝑈)) ∈ (LSubSp‘𝑇)) |
17 | | eqid 2737 |
. . . . . 6
⊢
(LSubSp‘𝑆) =
(LSubSp‘𝑆) |
18 | 17, 13 | lmhmpreima 20085 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ (𝐿‘(𝐹 “ 𝑈)) ∈ (LSubSp‘𝑇)) → (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈))) ∈ (LSubSp‘𝑆)) |
19 | 16, 18 | syldan 594 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈))) ∈ (LSubSp‘𝑆)) |
20 | | incom 4115 |
. . . . . . 7
⊢ (dom
𝐹 ∩ 𝑈) = (𝑈 ∩ dom 𝐹) |
21 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ 𝑉) |
22 | 4 | fdmd 6556 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → dom 𝐹 = 𝑉) |
23 | 21, 22 | sseqtrrd 3942 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ dom 𝐹) |
24 | | df-ss 3883 |
. . . . . . . 8
⊢ (𝑈 ⊆ dom 𝐹 ↔ (𝑈 ∩ dom 𝐹) = 𝑈) |
25 | 23, 24 | sylib 221 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝑈 ∩ dom 𝐹) = 𝑈) |
26 | 20, 25 | eqtr2id 2791 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑈 = (dom 𝐹 ∩ 𝑈)) |
27 | | dminss 6016 |
. . . . . 6
⊢ (dom
𝐹 ∩ 𝑈) ⊆ (◡𝐹 “ (𝐹 “ 𝑈)) |
28 | 26, 27 | eqsstrdi 3955 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ (◡𝐹 “ (𝐹 “ 𝑈))) |
29 | 2, 14 | lspssid 20022 |
. . . . . . 7
⊢ ((𝑇 ∈ LMod ∧ (𝐹 “ 𝑈) ⊆ (Base‘𝑇)) → (𝐹 “ 𝑈) ⊆ (𝐿‘(𝐹 “ 𝑈))) |
30 | 9, 12, 29 | syl2anc 587 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ 𝑈) ⊆ (𝐿‘(𝐹 “ 𝑈))) |
31 | | imass2 5970 |
. . . . . 6
⊢ ((𝐹 “ 𝑈) ⊆ (𝐿‘(𝐹 “ 𝑈)) → (◡𝐹 “ (𝐹 “ 𝑈)) ⊆ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈)))) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (◡𝐹 “ (𝐹 “ 𝑈)) ⊆ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈)))) |
33 | 28, 32 | sstrd 3911 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈)))) |
34 | | lmhmlsp.k |
. . . . 5
⊢ 𝐾 = (LSpan‘𝑆) |
35 | 17, 34 | lspssp 20025 |
. . . 4
⊢ ((𝑆 ∈ LMod ∧ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈))) ∈ (LSubSp‘𝑆) ∧ 𝑈 ⊆ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈)))) → (𝐾‘𝑈) ⊆ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈)))) |
36 | 7, 19, 33, 35 | syl3anc 1373 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐾‘𝑈) ⊆ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈)))) |
37 | | funimass2 6463 |
. . 3
⊢ ((Fun
𝐹 ∧ (𝐾‘𝑈) ⊆ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈)))) → (𝐹 “ (𝐾‘𝑈)) ⊆ (𝐿‘(𝐹 “ 𝑈))) |
38 | 5, 36, 37 | syl2anc 587 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ (𝐾‘𝑈)) ⊆ (𝐿‘(𝐹 “ 𝑈))) |
39 | 1, 17, 34 | lspcl 20013 |
. . . . 5
⊢ ((𝑆 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝐾‘𝑈) ∈ (LSubSp‘𝑆)) |
40 | 7, 21, 39 | syl2anc 587 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐾‘𝑈) ∈ (LSubSp‘𝑆)) |
41 | 17, 13 | lmhmima 20084 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ (𝐾‘𝑈) ∈ (LSubSp‘𝑆)) → (𝐹 “ (𝐾‘𝑈)) ∈ (LSubSp‘𝑇)) |
42 | 40, 41 | syldan 594 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ (𝐾‘𝑈)) ∈ (LSubSp‘𝑇)) |
43 | 1, 34 | lspssid 20022 |
. . . . 5
⊢ ((𝑆 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ (𝐾‘𝑈)) |
44 | 7, 21, 43 | syl2anc 587 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ (𝐾‘𝑈)) |
45 | | imass2 5970 |
. . . 4
⊢ (𝑈 ⊆ (𝐾‘𝑈) → (𝐹 “ 𝑈) ⊆ (𝐹 “ (𝐾‘𝑈))) |
46 | 44, 45 | syl 17 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ 𝑈) ⊆ (𝐹 “ (𝐾‘𝑈))) |
47 | 13, 14 | lspssp 20025 |
. . 3
⊢ ((𝑇 ∈ LMod ∧ (𝐹 “ (𝐾‘𝑈)) ∈ (LSubSp‘𝑇) ∧ (𝐹 “ 𝑈) ⊆ (𝐹 “ (𝐾‘𝑈))) → (𝐿‘(𝐹 “ 𝑈)) ⊆ (𝐹 “ (𝐾‘𝑈))) |
48 | 9, 42, 46, 47 | syl3anc 1373 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐿‘(𝐹 “ 𝑈)) ⊆ (𝐹 “ (𝐾‘𝑈))) |
49 | 38, 48 | eqssd 3918 |
1
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ (𝐾‘𝑈)) = (𝐿‘(𝐹 “ 𝑈))) |