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=\mathrm{Scalar}\left(S\right)$$
	islmhm.l	$$⊢L=\mathrm{Scalar}\left(T\right)$$
	islmhm.b	$$⊢B={\mathrm{Base}}_K$$
	islmhm.e	$$⊢E={\mathrm{Base}}_S$$
	islmhm.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	islmhm.n	$$⊢\underset{\dot{}}{\times }={\cdot }_T$$
Assertion	islmhm3	$$⊢\left(S\in \mathrm{LMod}\wedge T\in \mathrm{LMod}\right)\to \left(F\in \left(S\mathrm{LMHom}T\right)\leftrightarrow \left(F\in \left(S\mathrm{GrpHom}T\right)\wedge L=K\wedge \forall x\in B\forall y\in EF\left(x\underset{\dot{}}{·}y\right)=x\underset{\dot{}}{\times }F\left(y\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		islmhm.k	$$⊢K=\mathrm{Scalar}\left(S\right)$$
2		islmhm.l	$$⊢L=\mathrm{Scalar}\left(T\right)$$
3		islmhm.b	$$⊢B={\mathrm{Base}}_K$$
4		islmhm.e	$$⊢E={\mathrm{Base}}_S$$
5		islmhm.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
6		islmhm.n	$$⊢\underset{\dot{}}{\times }={\cdot }_T$$
7	1 2 3 4 5 6	islmhm	$$⊢F\in \left(S\mathrm{LMHom}T\right)\leftrightarrow \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 x\in B\forall y\in EF\left(x\underset{\dot{}}{·}y\right)=x\underset{\dot{}}{\times }F\left(y\right)\right)\right)$$
8	7	baib	$$⊢\left(S\in \mathrm{LMod}\wedge T\in \mathrm{LMod}\right)\to \left(F\in \left(S\mathrm{LMHom}T\right)\leftrightarrow \left(F\in \left(S\mathrm{GrpHom}T\right)\wedge L=K\wedge \forall x\in B\forall y\in EF\left(x\underset{\dot{}}{·}y\right)=x\underset{\dot{}}{\times }F\left(y\right)\right)\right)$$