Metamath Proof Explorer

Theorem reslmhm2

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 reslmhm2 
|- ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) -> F e. ( S LMHom T ) )

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 ` T ) = ( .s ` T )
6 eqid 
 |-  ( Scalar ` S ) = ( Scalar ` S )
7 eqid 
 |-  ( Scalar ` T ) = ( Scalar ` T )
8 eqid 
 |-  ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` S ) )
9 lmhmlmod1 
 |-  ( F e. ( S LMHom U ) -> S e. LMod )
10 9 3ad2ant1 
 |-  ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) -> S e. LMod )
11 simp2 
 |-  ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) -> T e. LMod )
12 1 7 resssca 
 |-  ( X e. L -> ( Scalar ` T ) = ( Scalar ` U ) )
13 12 3ad2ant3 
 |-  ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) -> ( Scalar ` T ) = ( Scalar ` U ) )
14 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
15 6 14 lmhmsca 
 |-  ( F e. ( S LMHom U ) -> ( Scalar ` U ) = ( Scalar ` S ) )
16 15 3ad2ant1 
 |-  ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) -> ( Scalar ` U ) = ( Scalar ` S ) )
17 13 16 eqtrd 
 |-  ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) -> ( Scalar ` T ) = ( Scalar ` S ) )
18 lmghm 
 |-  ( F e. ( S LMHom U ) -> F e. ( S GrpHom U ) )
19 18 3ad2ant1 
 |-  ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) -> F e. ( S GrpHom U ) )
20 2 lsssubg 
 |-  ( ( T e. LMod /\ X e. L ) -> X e. ( SubGrp ` T ) )
21 20 3adant1 
 |-  ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) -> X e. ( SubGrp ` T ) )
22 1 resghm2 
 |-  ( ( F e. ( S GrpHom U ) /\ X e. ( SubGrp ` T ) ) -> F e. ( S GrpHom T ) )
23 19 21 22 syl2anc 
 |-  ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) -> F e. ( S GrpHom T ) )
24 eqid 
 |-  ( .s ` U ) = ( .s ` U )
25 6 8 3 4 24 lmhmlin 
 |-  ( ( F e. ( S LMHom U ) /\ x e. ( Base ` ( Scalar ` S ) ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( .s ` S ) y ) ) = ( x ( .s ` U ) ( F ` y ) ) )
26 25 3expb 
 |-  ( ( F e. ( S LMHom U ) /\ ( x e. ( Base ` ( Scalar ` S ) ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( .s ` S ) y ) ) = ( x ( .s ` U ) ( F ` y ) ) )
27 26 3ad2antl1 
 |-  ( ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) /\ ( x e. ( Base ` ( Scalar ` S ) ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( .s ` S ) y ) ) = ( x ( .s ` U ) ( F ` y ) ) )
28 simpl3 
 |-  ( ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) /\ ( x e. ( Base ` ( Scalar ` S ) ) /\ y e. ( Base ` S ) ) ) -> X e. L )
29 1 5 ressvsca 
 |-  ( X e. L -> ( .s ` T ) = ( .s ` U ) )
30 29 oveqd 
 |-  ( X e. L -> ( x ( .s ` T ) ( F ` y ) ) = ( x ( .s ` U ) ( F ` y ) ) )
31 28 30 syl 
 |-  ( ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) /\ ( x e. ( Base ` ( Scalar ` S ) ) /\ y e. ( Base ` S ) ) ) -> ( x ( .s ` T ) ( F ` y ) ) = ( x ( .s ` U ) ( F ` y ) ) )
32 27 31 eqtr4d 
 |-  ( ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) /\ ( x e. ( Base ` ( Scalar ` S ) ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( .s ` S ) y ) ) = ( x ( .s ` T ) ( F ` y ) ) )
33 3 4 5 6 7 8 10 11 17 23 32 islmhmd 
 |-  ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) -> F e. ( S LMHom T ) )