# 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}=\mathrm{Scalar}\left({S}\right)$
lmhmlem.l ${⊢}{L}=\mathrm{Scalar}\left({T}\right)$
Assertion lmhmlem ${⊢}{F}\in \left({S}\mathrm{LMHom}{T}\right)\to \left(\left({S}\in \mathrm{LMod}\wedge {T}\in \mathrm{LMod}\right)\wedge \left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {L}={K}\right)\right)$

### Proof

Step Hyp Ref Expression
1 lmhmlem.k ${⊢}{K}=\mathrm{Scalar}\left({S}\right)$
2 lmhmlem.l ${⊢}{L}=\mathrm{Scalar}\left({T}\right)$
3 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
4 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
5 eqid ${⊢}{\cdot }_{{S}}={\cdot }_{{S}}$
6 eqid ${⊢}{\cdot }_{{T}}={\cdot }_{{T}}$
7 1 2 3 4 5 6 islmhm ${⊢}{F}\in \left({S}\mathrm{LMHom}{T}\right)↔\left(\left({S}\in \mathrm{LMod}\wedge {T}\in \mathrm{LMod}\right)\wedge \left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {L}={K}\wedge \forall {a}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}{F}\left({a}{\cdot }_{{S}}{b}\right)={a}{\cdot }_{{T}}{F}\left({b}\right)\right)\right)$
8 3simpa ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {L}={K}\wedge \forall {a}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}{F}\left({a}{\cdot }_{{S}}{b}\right)={a}{\cdot }_{{T}}{F}\left({b}\right)\right)\to \left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {L}={K}\right)$
9 8 anim2i ${⊢}\left(\left({S}\in \mathrm{LMod}\wedge {T}\in \mathrm{LMod}\right)\wedge \left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {L}={K}\wedge \forall {a}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}{F}\left({a}{\cdot }_{{S}}{b}\right)={a}{\cdot }_{{T}}{F}\left({b}\right)\right)\right)\to \left(\left({S}\in \mathrm{LMod}\wedge {T}\in \mathrm{LMod}\right)\wedge \left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {L}={K}\right)\right)$
10 7 9 sylbi ${⊢}{F}\in \left({S}\mathrm{LMHom}{T}\right)\to \left(\left({S}\in \mathrm{LMod}\wedge {T}\in \mathrm{LMod}\right)\wedge \left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {L}={K}\right)\right)$