Proof of Theorem lmhmlsp
Step | Hyp | Ref
| Expression |
1 | | lmhmlsp.v |
. . . . . 6
⊢ 𝑉 = (Base‘𝑆) |
2 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝑇) =
(Base‘𝑇) |
3 | 1, 2 | lmhmf 19034 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝑉⟶(Base‘𝑇)) |
4 | 3 | adantr 481 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝐹:𝑉⟶(Base‘𝑇)) |
5 | | ffun 6048 |
. . . 4
⊢ (𝐹:𝑉⟶(Base‘𝑇) → Fun 𝐹) |
6 | 4, 5 | syl 17 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → Fun 𝐹) |
7 | | lmhmlmod1 19033 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) |
8 | 7 | adantr 481 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑆 ∈ LMod) |
9 | | lmhmlmod2 19032 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) |
10 | 9 | adantr 481 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑇 ∈ LMod) |
11 | | imassrn 5477 |
. . . . . . 7
⊢ (𝐹 “ 𝑈) ⊆ ran 𝐹 |
12 | | frn 6053 |
. . . . . . . 8
⊢ (𝐹:𝑉⟶(Base‘𝑇) → ran 𝐹 ⊆ (Base‘𝑇)) |
13 | 4, 12 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → ran 𝐹 ⊆ (Base‘𝑇)) |
14 | 11, 13 | syl5ss 3614 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ 𝑈) ⊆ (Base‘𝑇)) |
15 | | eqid 2622 |
. . . . . . 7
⊢
(LSubSp‘𝑇) =
(LSubSp‘𝑇) |
16 | | lmhmlsp.l |
. . . . . . 7
⊢ 𝐿 = (LSpan‘𝑇) |
17 | 2, 15, 16 | lspcl 18976 |
. . . . . 6
⊢ ((𝑇 ∈ LMod ∧ (𝐹 “ 𝑈) ⊆ (Base‘𝑇)) → (𝐿‘(𝐹 “ 𝑈)) ∈ (LSubSp‘𝑇)) |
18 | 10, 14, 17 | syl2anc 693 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐿‘(𝐹 “ 𝑈)) ∈ (LSubSp‘𝑇)) |
19 | | eqid 2622 |
. . . . . 6
⊢
(LSubSp‘𝑆) =
(LSubSp‘𝑆) |
20 | 19, 15 | lmhmpreima 19048 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ (𝐿‘(𝐹 “ 𝑈)) ∈ (LSubSp‘𝑇)) → (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈))) ∈ (LSubSp‘𝑆)) |
21 | 18, 20 | syldan 487 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈))) ∈ (LSubSp‘𝑆)) |
22 | | incom 3805 |
. . . . . . 7
⊢ (dom
𝐹 ∩ 𝑈) = (𝑈 ∩ dom 𝐹) |
23 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ 𝑉) |
24 | | fdm 6051 |
. . . . . . . . . 10
⊢ (𝐹:𝑉⟶(Base‘𝑇) → dom 𝐹 = 𝑉) |
25 | 4, 24 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → dom 𝐹 = 𝑉) |
26 | 23, 25 | sseqtr4d 3642 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ dom 𝐹) |
27 | | df-ss 3588 |
. . . . . . . 8
⊢ (𝑈 ⊆ dom 𝐹 ↔ (𝑈 ∩ dom 𝐹) = 𝑈) |
28 | 26, 27 | sylib 208 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝑈 ∩ dom 𝐹) = 𝑈) |
29 | 22, 28 | syl5req 2669 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑈 = (dom 𝐹 ∩ 𝑈)) |
30 | | dminss 5547 |
. . . . . 6
⊢ (dom
𝐹 ∩ 𝑈) ⊆ (◡𝐹 “ (𝐹 “ 𝑈)) |
31 | 29, 30 | syl6eqss 3655 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ (◡𝐹 “ (𝐹 “ 𝑈))) |
32 | 2, 16 | lspssid 18985 |
. . . . . . 7
⊢ ((𝑇 ∈ LMod ∧ (𝐹 “ 𝑈) ⊆ (Base‘𝑇)) → (𝐹 “ 𝑈) ⊆ (𝐿‘(𝐹 “ 𝑈))) |
33 | 10, 14, 32 | syl2anc 693 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ 𝑈) ⊆ (𝐿‘(𝐹 “ 𝑈))) |
34 | | imass2 5501 |
. . . . . 6
⊢ ((𝐹 “ 𝑈) ⊆ (𝐿‘(𝐹 “ 𝑈)) → (◡𝐹 “ (𝐹 “ 𝑈)) ⊆ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈)))) |
35 | 33, 34 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (◡𝐹 “ (𝐹 “ 𝑈)) ⊆ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈)))) |
36 | 31, 35 | sstrd 3613 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈)))) |
37 | | lmhmlsp.k |
. . . . 5
⊢ 𝐾 = (LSpan‘𝑆) |
38 | 19, 37 | lspssp 18988 |
. . . 4
⊢ ((𝑆 ∈ LMod ∧ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈))) ∈ (LSubSp‘𝑆) ∧ 𝑈 ⊆ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈)))) → (𝐾‘𝑈) ⊆ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈)))) |
39 | 8, 21, 36, 38 | syl3anc 1326 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐾‘𝑈) ⊆ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈)))) |
40 | | funimass2 5972 |
. . 3
⊢ ((Fun
𝐹 ∧ (𝐾‘𝑈) ⊆ (◡𝐹 “ (𝐿‘(𝐹 “ 𝑈)))) → (𝐹 “ (𝐾‘𝑈)) ⊆ (𝐿‘(𝐹 “ 𝑈))) |
41 | 6, 39, 40 | syl2anc 693 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ (𝐾‘𝑈)) ⊆ (𝐿‘(𝐹 “ 𝑈))) |
42 | 1, 19, 37 | lspcl 18976 |
. . . . 5
⊢ ((𝑆 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝐾‘𝑈) ∈ (LSubSp‘𝑆)) |
43 | 8, 23, 42 | syl2anc 693 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐾‘𝑈) ∈ (LSubSp‘𝑆)) |
44 | 19, 15 | lmhmima 19047 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ (𝐾‘𝑈) ∈ (LSubSp‘𝑆)) → (𝐹 “ (𝐾‘𝑈)) ∈ (LSubSp‘𝑇)) |
45 | 43, 44 | syldan 487 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ (𝐾‘𝑈)) ∈ (LSubSp‘𝑇)) |
46 | 1, 37 | lspssid 18985 |
. . . . 5
⊢ ((𝑆 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ (𝐾‘𝑈)) |
47 | 8, 23, 46 | syl2anc 693 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ (𝐾‘𝑈)) |
48 | | imass2 5501 |
. . . 4
⊢ (𝑈 ⊆ (𝐾‘𝑈) → (𝐹 “ 𝑈) ⊆ (𝐹 “ (𝐾‘𝑈))) |
49 | 47, 48 | syl 17 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ 𝑈) ⊆ (𝐹 “ (𝐾‘𝑈))) |
50 | 15, 16 | lspssp 18988 |
. . 3
⊢ ((𝑇 ∈ LMod ∧ (𝐹 “ (𝐾‘𝑈)) ∈ (LSubSp‘𝑇) ∧ (𝐹 “ 𝑈) ⊆ (𝐹 “ (𝐾‘𝑈))) → (𝐿‘(𝐹 “ 𝑈)) ⊆ (𝐹 “ (𝐾‘𝑈))) |
51 | 10, 45, 49, 50 | syl3anc 1326 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐿‘(𝐹 “ 𝑈)) ⊆ (𝐹 “ (𝐾‘𝑈))) |
52 | 41, 51 | eqssd 3620 |
1
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ (𝐾‘𝑈)) = (𝐿‘(𝐹 “ 𝑈))) |