Metamath Proof Explorer

Theorem islmhm3

Description: Property of a module homomorphism, similar to ismhm . (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Hypotheses islmhm.k 
|- K = ( Scalar ` S )
islmhm.l 
|- L = ( Scalar ` T )
islmhm.b 
|- B = ( Base ` K )
islmhm.e 
|- E = ( Base ` S )
islmhm.m 
|- .x. = ( .s ` S )
islmhm.n 
|- .X. = ( .s ` T )
Assertion islmhm3 
|- ( ( S e. LMod /\ T e. LMod ) -> ( F e. ( S LMHom T ) <-> ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 islmhm.k 
 |-  K = ( Scalar ` S )
2 islmhm.l 
 |-  L = ( Scalar ` T )
3 islmhm.b 
 |-  B = ( Base ` K )
4 islmhm.e 
 |-  E = ( Base ` S )
5 islmhm.m 
 |-  .x. = ( .s ` S )
6 islmhm.n 
 |-  .X. = ( .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. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )
8 7 baib 
 |-  ( ( S e. LMod /\ T e. LMod ) -> ( F e. ( S LMHom T ) <-> ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )