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