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 e. ( S LMHom T ) /\ U C_ 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 e. ( S LMHom T ) -> F : V --> ( Base ` T ) )
6 5 adantr 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> F : V --> ( Base ` T ) )
7 6 ffund 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> Fun F )
8 lmhmlmod1 
 |-  ( F e. ( S LMHom T ) -> S e. LMod )
9 8 adantr 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> S e. LMod )
10 lmhmlmod2 
 |-  ( F e. ( S LMHom T ) -> T e. LMod )
11 10 adantr 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> T e. LMod )
12 imassrn 
 |-  ( F " U ) C_ ran F
13 6 frnd 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> ran F C_ ( Base ` T ) )
14 12 13 sstrid 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> ( F " U ) C_ ( Base ` T ) )
15 eqid 
 |-  ( LSubSp ` T ) = ( LSubSp ` T )
16 4 15 3 lspcl 
 |-  ( ( T e. LMod /\ ( F " U ) C_ ( Base ` T ) ) -> ( L ` ( F " U ) ) e. ( LSubSp ` T ) )
17 11 14 16 syl2anc 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> ( L ` ( F " U ) ) e. ( LSubSp ` T ) )
18 eqid 
 |-  ( LSubSp ` S ) = ( LSubSp ` S )
19 18 15 lmhmpreima 
 |-  ( ( F e. ( S LMHom T ) /\ ( L ` ( F " U ) ) e. ( LSubSp ` T ) ) -> ( `' F " ( L ` ( F " U ) ) ) e. ( LSubSp ` S ) )
20 17 19 syldan 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> ( `' F " ( L ` ( F " U ) ) ) e. ( LSubSp ` S ) )
21 incom 
 |-  ( dom F i^i U ) = ( U i^i dom F )
22 simpr 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> U C_ V )
23 6 fdmd 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> dom F = V )
24 22 23 sseqtrrd 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> U C_ dom F )
25 df-ss 
 |-  ( U C_ dom F <-> ( U i^i dom F ) = U )
26 24 25 sylib 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> ( U i^i dom F ) = U )
27 21 26 syl5req 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> U = ( dom F i^i U ) )
28 dminss 
 |-  ( dom F i^i U ) C_ ( `' F " ( F " U ) )
29 27 28 eqsstrdi 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> U C_ ( `' F " ( F " U ) ) )
30 4 3 lspssid 
 |-  ( ( T e. LMod /\ ( F " U ) C_ ( Base ` T ) ) -> ( F " U ) C_ ( L ` ( F " U ) ) )
31 11 14 30 syl2anc 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> ( F " U ) C_ ( L ` ( F " U ) ) )
32 imass2 
 |-  ( ( F " U ) C_ ( L ` ( F " U ) ) -> ( `' F " ( F " U ) ) C_ ( `' F " ( L ` ( F " U ) ) ) )
33 31 32 syl 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> ( `' F " ( F " U ) ) C_ ( `' F " ( L ` ( F " U ) ) ) )
34 29 33 sstrd 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> U C_ ( `' F " ( L ` ( F " U ) ) ) )
35 18 2 lspssp 
 |-  ( ( S e. LMod /\ ( `' F " ( L ` ( F " U ) ) ) e. ( LSubSp ` S ) /\ U C_ ( `' F " ( L ` ( F " U ) ) ) ) -> ( K ` U ) C_ ( `' F " ( L ` ( F " U ) ) ) )
36 9 20 34 35 syl3anc 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> ( K ` U ) C_ ( `' F " ( L ` ( F " U ) ) ) )
37 funimass2 
 |-  ( ( Fun F /\ ( K ` U ) C_ ( `' F " ( L ` ( F " U ) ) ) ) -> ( F " ( K ` U ) ) C_ ( L ` ( F " U ) ) )
38 7 36 37 syl2anc 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> ( F " ( K ` U ) ) C_ ( L ` ( F " U ) ) )
39 1 18 2 lspcl 
 |-  ( ( S e. LMod /\ U C_ V ) -> ( K ` U ) e. ( LSubSp ` S ) )
40 9 22 39 syl2anc 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> ( K ` U ) e. ( LSubSp ` S ) )
41 18 15 lmhmima 
 |-  ( ( F e. ( S LMHom T ) /\ ( K ` U ) e. ( LSubSp ` S ) ) -> ( F " ( K ` U ) ) e. ( LSubSp ` T ) )
42 40 41 syldan 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> ( F " ( K ` U ) ) e. ( LSubSp ` T ) )
43 1 2 lspssid 
 |-  ( ( S e. LMod /\ U C_ V ) -> U C_ ( K ` U ) )
44 9 22 43 syl2anc 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> U C_ ( K ` U ) )
45 imass2 
 |-  ( U C_ ( K ` U ) -> ( F " U ) C_ ( F " ( K ` U ) ) )
46 44 45 syl 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> ( F " U ) C_ ( F " ( K ` U ) ) )
47 15 3 lspssp 
 |-  ( ( T e. LMod /\ ( F " ( K ` U ) ) e. ( LSubSp ` T ) /\ ( F " U ) C_ ( F " ( K ` U ) ) ) -> ( L ` ( F " U ) ) C_ ( F " ( K ` U ) ) )
48 11 42 46 47 syl3anc 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> ( L ` ( F " U ) ) C_ ( F " ( K ` U ) ) )
49 38 48 eqssd 
 |-  ( ( F e. ( S LMHom T ) /\ U C_ V ) -> ( F " ( K ` U ) ) = ( L ` ( F " U ) ) )