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