Metamath Proof Explorer


Theorem lmhmlsp

Description: Homomorphisms preserve spans. (Contributed by Stefan O'Rear, 1-Jan-2015)

Ref Expression
Hypotheses lmhmlsp.v 𝑉 = ( Base ‘ 𝑆 )
lmhmlsp.k 𝐾 = ( LSpan ‘ 𝑆 )
lmhmlsp.l 𝐿 = ( LSpan ‘ 𝑇 )
Assertion lmhmlsp ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → ( 𝐹 “ ( 𝐾𝑈 ) ) = ( 𝐿 ‘ ( 𝐹𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 lmhmlsp.v 𝑉 = ( Base ‘ 𝑆 )
2 lmhmlsp.k 𝐾 = ( LSpan ‘ 𝑆 )
3 lmhmlsp.l 𝐿 = ( LSpan ‘ 𝑇 )
4 eqid ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
5 1 4 lmhmf ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
6 5 adantr ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
7 6 ffund ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → Fun 𝐹 )
8 lmhmlmod1 ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
9 8 adantr ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → 𝑆 ∈ LMod )
10 lmhmlmod2 ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod )
11 10 adantr ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → 𝑇 ∈ LMod )
12 imassrn ( 𝐹𝑈 ) ⊆ ran 𝐹
13 6 frnd ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → ran 𝐹 ⊆ ( Base ‘ 𝑇 ) )
14 12 13 sstrid ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → ( 𝐹𝑈 ) ⊆ ( Base ‘ 𝑇 ) )
15 eqid ( LSubSp ‘ 𝑇 ) = ( LSubSp ‘ 𝑇 )
16 4 15 3 lspcl ( ( 𝑇 ∈ LMod ∧ ( 𝐹𝑈 ) ⊆ ( Base ‘ 𝑇 ) ) → ( 𝐿 ‘ ( 𝐹𝑈 ) ) ∈ ( LSubSp ‘ 𝑇 ) )
17 11 14 16 syl2anc ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → ( 𝐿 ‘ ( 𝐹𝑈 ) ) ∈ ( LSubSp ‘ 𝑇 ) )
18 eqid ( LSubSp ‘ 𝑆 ) = ( LSubSp ‘ 𝑆 )
19 18 15 lmhmpreima ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ( 𝐿 ‘ ( 𝐹𝑈 ) ) ∈ ( LSubSp ‘ 𝑇 ) ) → ( 𝐹 “ ( 𝐿 ‘ ( 𝐹𝑈 ) ) ) ∈ ( LSubSp ‘ 𝑆 ) )
20 17 19 syldan ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → ( 𝐹 “ ( 𝐿 ‘ ( 𝐹𝑈 ) ) ) ∈ ( LSubSp ‘ 𝑆 ) )
21 incom ( dom 𝐹𝑈 ) = ( 𝑈 ∩ dom 𝐹 )
22 simpr ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → 𝑈𝑉 )
23 6 fdmd ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → dom 𝐹 = 𝑉 )
24 22 23 sseqtrrd ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → 𝑈 ⊆ dom 𝐹 )
25 df-ss ( 𝑈 ⊆ dom 𝐹 ↔ ( 𝑈 ∩ dom 𝐹 ) = 𝑈 )
26 24 25 sylib ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → ( 𝑈 ∩ dom 𝐹 ) = 𝑈 )
27 21 26 eqtr2id ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → 𝑈 = ( dom 𝐹𝑈 ) )
28 dminss ( dom 𝐹𝑈 ) ⊆ ( 𝐹 “ ( 𝐹𝑈 ) )
29 27 28 eqsstrdi ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → 𝑈 ⊆ ( 𝐹 “ ( 𝐹𝑈 ) ) )
30 4 3 lspssid ( ( 𝑇 ∈ LMod ∧ ( 𝐹𝑈 ) ⊆ ( Base ‘ 𝑇 ) ) → ( 𝐹𝑈 ) ⊆ ( 𝐿 ‘ ( 𝐹𝑈 ) ) )
31 11 14 30 syl2anc ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → ( 𝐹𝑈 ) ⊆ ( 𝐿 ‘ ( 𝐹𝑈 ) ) )
32 imass2 ( ( 𝐹𝑈 ) ⊆ ( 𝐿 ‘ ( 𝐹𝑈 ) ) → ( 𝐹 “ ( 𝐹𝑈 ) ) ⊆ ( 𝐹 “ ( 𝐿 ‘ ( 𝐹𝑈 ) ) ) )
33 31 32 syl ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → ( 𝐹 “ ( 𝐹𝑈 ) ) ⊆ ( 𝐹 “ ( 𝐿 ‘ ( 𝐹𝑈 ) ) ) )
34 29 33 sstrd ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → 𝑈 ⊆ ( 𝐹 “ ( 𝐿 ‘ ( 𝐹𝑈 ) ) ) )
35 18 2 lspssp ( ( 𝑆 ∈ LMod ∧ ( 𝐹 “ ( 𝐿 ‘ ( 𝐹𝑈 ) ) ) ∈ ( LSubSp ‘ 𝑆 ) ∧ 𝑈 ⊆ ( 𝐹 “ ( 𝐿 ‘ ( 𝐹𝑈 ) ) ) ) → ( 𝐾𝑈 ) ⊆ ( 𝐹 “ ( 𝐿 ‘ ( 𝐹𝑈 ) ) ) )
36 9 20 34 35 syl3anc ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → ( 𝐾𝑈 ) ⊆ ( 𝐹 “ ( 𝐿 ‘ ( 𝐹𝑈 ) ) ) )
37 funimass2 ( ( Fun 𝐹 ∧ ( 𝐾𝑈 ) ⊆ ( 𝐹 “ ( 𝐿 ‘ ( 𝐹𝑈 ) ) ) ) → ( 𝐹 “ ( 𝐾𝑈 ) ) ⊆ ( 𝐿 ‘ ( 𝐹𝑈 ) ) )
38 7 36 37 syl2anc ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → ( 𝐹 “ ( 𝐾𝑈 ) ) ⊆ ( 𝐿 ‘ ( 𝐹𝑈 ) ) )
39 1 18 2 lspcl ( ( 𝑆 ∈ LMod ∧ 𝑈𝑉 ) → ( 𝐾𝑈 ) ∈ ( LSubSp ‘ 𝑆 ) )
40 9 22 39 syl2anc ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → ( 𝐾𝑈 ) ∈ ( LSubSp ‘ 𝑆 ) )
41 18 15 lmhmima ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ( 𝐾𝑈 ) ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝐹 “ ( 𝐾𝑈 ) ) ∈ ( LSubSp ‘ 𝑇 ) )
42 40 41 syldan ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → ( 𝐹 “ ( 𝐾𝑈 ) ) ∈ ( LSubSp ‘ 𝑇 ) )
43 1 2 lspssid ( ( 𝑆 ∈ LMod ∧ 𝑈𝑉 ) → 𝑈 ⊆ ( 𝐾𝑈 ) )
44 9 22 43 syl2anc ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → 𝑈 ⊆ ( 𝐾𝑈 ) )
45 imass2 ( 𝑈 ⊆ ( 𝐾𝑈 ) → ( 𝐹𝑈 ) ⊆ ( 𝐹 “ ( 𝐾𝑈 ) ) )
46 44 45 syl ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → ( 𝐹𝑈 ) ⊆ ( 𝐹 “ ( 𝐾𝑈 ) ) )
47 15 3 lspssp ( ( 𝑇 ∈ LMod ∧ ( 𝐹 “ ( 𝐾𝑈 ) ) ∈ ( LSubSp ‘ 𝑇 ) ∧ ( 𝐹𝑈 ) ⊆ ( 𝐹 “ ( 𝐾𝑈 ) ) ) → ( 𝐿 ‘ ( 𝐹𝑈 ) ) ⊆ ( 𝐹 “ ( 𝐾𝑈 ) ) )
48 11 42 46 47 syl3anc ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → ( 𝐿 ‘ ( 𝐹𝑈 ) ) ⊆ ( 𝐹 “ ( 𝐾𝑈 ) ) )
49 38 48 eqssd ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈𝑉 ) → ( 𝐹 “ ( 𝐾𝑈 ) ) = ( 𝐿 ‘ ( 𝐹𝑈 ) ) )