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 ) ) )