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 𝑇 ) ∧ 𝑈 ⊆ 𝑉 ) → ( 𝐹 “ ( 𝐾 ‘ 𝑈 ) ) = ( 𝐿 ‘ ( 𝐹 “ 𝑈 ) ) )