Metamath Proof Explorer

Theorem lmhmlsp

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

Ref Expression
Hypotheses lmhmlsp.v ⊢ V = Base S
lmhmlsp.k ⊢ K = LSpan ⁡ S
lmhmlsp.l ⊢ L = LSpan ⁡ T
Assertion lmhmlsp ⊢ F ∈ S LMHom T ∧ U ⊆ V → F K ⁡ U = L ⁡ F U

Proof

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