Metamath Proof Explorer

Theorem reslmhm2b

Description: Expansion of the codomain of a homomorphism. (Contributed by Stefan O'Rear, 3-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

Ref Expression
Hypotheses reslmhm2.u 
|- U = ( T |`s X )
reslmhm2.l 
|- L = ( LSubSp ` T )
Assertion reslmhm2b 
|- ( ( T e. LMod /\ X e. L /\ ran F C_ X ) -> ( F e. ( S LMHom T ) <-> F e. ( S LMHom U ) ) )

Proof

Step Hyp Ref Expression
1 reslmhm2.u 
 |-  U = ( T |`s X )
2 reslmhm2.l 
 |-  L = ( LSubSp ` T )
3 eqid 
 |-  ( Base ` S ) = ( Base ` S )
4 eqid 
 |-  ( .s ` S ) = ( .s ` S )
5 eqid 
 |-  ( .s ` U ) = ( .s ` U )
6 eqid 
 |-  ( Scalar ` S ) = ( Scalar ` S )
7 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
8 eqid 
 |-  ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` S ) )
9 lmhmlmod1 
 |-  ( F e. ( S LMHom T ) -> S e. LMod )
10 9 adantl 
 |-  ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S LMHom T ) ) -> S e. LMod )
11 simpl1 
 |-  ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S LMHom T ) ) -> T e. LMod )
12 simpl2 
 |-  ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S LMHom T ) ) -> X e. L )
13 1 2 lsslmod 
 |-  ( ( T e. LMod /\ X e. L ) -> U e. LMod )
14 11 12 13 syl2anc 
 |-  ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S LMHom T ) ) -> U e. LMod )
15 eqid 
 |-  ( Scalar ` T ) = ( Scalar ` T )
16 1 15 resssca 
 |-  ( X e. L -> ( Scalar ` T ) = ( Scalar ` U ) )
17 16 3ad2ant2 
 |-  ( ( T e. LMod /\ X e. L /\ ran F C_ X ) -> ( Scalar ` T ) = ( Scalar ` U ) )
18 6 15 lmhmsca 
 |-  ( F e. ( S LMHom T ) -> ( Scalar ` T ) = ( Scalar ` S ) )
19 17 18 sylan9req 
 |-  ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S LMHom T ) ) -> ( Scalar ` U ) = ( Scalar ` S ) )
20 lmghm 
 |-  ( F e. ( S LMHom T ) -> F e. ( S GrpHom T ) )
21 2 lsssubg 
 |-  ( ( T e. LMod /\ X e. L ) -> X e. ( SubGrp ` T ) )
22 1 resghm2b 
 |-  ( ( X e. ( SubGrp ` T ) /\ ran F C_ X ) -> ( F e. ( S GrpHom T ) <-> F e. ( S GrpHom U ) ) )
23 21 22 stoic3 
 |-  ( ( T e. LMod /\ X e. L /\ ran F C_ X ) -> ( F e. ( S GrpHom T ) <-> F e. ( S GrpHom U ) ) )
24 23 biimpa 
 |-  ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S GrpHom T ) ) -> F e. ( S GrpHom U ) )
25 20 24 sylan2 
 |-  ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S LMHom T ) ) -> F e. ( S GrpHom U ) )
26 eqid 
 |-  ( .s ` T ) = ( .s ` T )
27 6 8 3 4 26 lmhmlin 
 |-  ( ( F e. ( S LMHom T ) /\ x e. ( Base ` ( Scalar ` S ) ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( .s ` S ) y ) ) = ( x ( .s ` T ) ( F ` y ) ) )
28 27 3expb 
 |-  ( ( F e. ( S LMHom T ) /\ ( x e. ( Base ` ( Scalar ` S ) ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( .s ` S ) y ) ) = ( x ( .s ` T ) ( F ` y ) ) )
29 28 adantll 
 |-  ( ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S LMHom T ) ) /\ ( x e. ( Base ` ( Scalar ` S ) ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( .s ` S ) y ) ) = ( x ( .s ` T ) ( F ` y ) ) )
30 simpll2 
 |-  ( ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S LMHom T ) ) /\ ( x e. ( Base ` ( Scalar ` S ) ) /\ y e. ( Base ` S ) ) ) -> X e. L )
31 1 26 ressvsca 
 |-  ( X e. L -> ( .s ` T ) = ( .s ` U ) )
32 31 oveqd 
 |-  ( X e. L -> ( x ( .s ` T ) ( F ` y ) ) = ( x ( .s ` U ) ( F ` y ) ) )
33 30 32 syl 
 |-  ( ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S LMHom T ) ) /\ ( x e. ( Base ` ( Scalar ` S ) ) /\ y e. ( Base ` S ) ) ) -> ( x ( .s ` T ) ( F ` y ) ) = ( x ( .s ` U ) ( F ` y ) ) )
34 29 33 eqtrd 
 |-  ( ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S LMHom T ) ) /\ ( x e. ( Base ` ( Scalar ` S ) ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( .s ` S ) y ) ) = ( x ( .s ` U ) ( F ` y ) ) )
35 3 4 5 6 7 8 10 14 19 25 34 islmhmd 
 |-  ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S LMHom T ) ) -> F e. ( S LMHom U ) )
36 simpr 
 |-  ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S LMHom U ) ) -> F e. ( S LMHom U ) )
37 simpl1 
 |-  ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S LMHom U ) ) -> T e. LMod )
38 simpl2 
 |-  ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S LMHom U ) ) -> X e. L )
39 1 2 reslmhm2 
 |-  ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) -> F e. ( S LMHom T ) )
40 36 37 38 39 syl3anc 
 |-  ( ( ( T e. LMod /\ X e. L /\ ran F C_ X ) /\ F e. ( S LMHom U ) ) -> F e. ( S LMHom T ) )
41 35 40 impbida 
 |-  ( ( T e. LMod /\ X e. L /\ ran F C_ X ) -> ( F e. ( S LMHom T ) <-> F e. ( S LMHom U ) ) )