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	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	islmhm.n	$⊢ \underset{˙}{\times} = \cdot_{T}$
Assertion	islmhm3	$⊢ (S \in LMod \land T \in LMod) \to (F \in (S LMHom T) \leftrightarrow (F \in (S GrpHom T) \land L = K \land \forall x \in B \forall y \in E F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} 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	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
6		islmhm.n	$⊢ \underset{˙}{\times} = \cdot_{T}$
7	1 2 3 4 5 6	islmhm	$⊢ F \in (S LMHom T) \leftrightarrow ((S \in LMod \land T \in LMod) \land (F \in (S GrpHom T) \land L = K \land \forall x \in B \forall y \in E F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)))$
8	7	baib	$⊢ (S \in LMod \land T \in LMod) \to (F \in (S LMHom T) \leftrightarrow (F \in (S GrpHom T) \land L = K \land \forall x \in B \forall y \in E F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)))$

Metamath Proof Explorer