Metamath Proof Explorer

Theorem lmhmlem

Description: Non-quantified consequences of a left module homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015)

Ref Expression
Hypotheses lmhmlem.k 
|- K = ( Scalar ` S )
lmhmlem.l 
|- L = ( Scalar ` T )
Assertion lmhmlem 
|- ( F e. ( S LMHom T ) -> ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ L = K ) ) )

Proof

Step Hyp Ref Expression
1 lmhmlem.k 
 |-  K = ( Scalar ` S )
2 lmhmlem.l 
 |-  L = ( Scalar ` T )
3 eqid 
 |-  ( Base ` K ) = ( Base ` K )
4 eqid 
 |-  ( Base ` S ) = ( Base ` S )
5 eqid 
 |-  ( .s ` S ) = ( .s ` S )
6 eqid 
 |-  ( .s ` T ) = ( .s ` T )
7 1 2 3 4 5 6 islmhm 
 |-  ( F e. ( S LMHom T ) <-> ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ L = K /\ A. a e. ( Base ` K ) A. b e. ( Base ` S ) ( F ` ( a ( .s ` S ) b ) ) = ( a ( .s ` T ) ( F ` b ) ) ) ) )
8 3simpa 
 |-  ( ( F e. ( S GrpHom T ) /\ L = K /\ A. a e. ( Base ` K ) A. b e. ( Base ` S ) ( F ` ( a ( .s ` S ) b ) ) = ( a ( .s ` T ) ( F ` b ) ) ) -> ( F e. ( S GrpHom T ) /\ L = K ) )
9 8 anim2i 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ L = K /\ A. a e. ( Base ` K ) A. b e. ( Base ` S ) ( F ` ( a ( .s ` S ) b ) ) = ( a ( .s ` T ) ( F ` b ) ) ) ) -> ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ L = K ) ) )
10 7 9 sylbi 
 |-  ( F e. ( S LMHom T ) -> ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ L = K ) ) )