lmhmlem

Description: Non-quantified consequences of a left module homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015)

	Ref	Expression
Hypotheses	lmhmlem.k	$⊢ K = Scalar (S)$
	lmhmlem.l	$⊢ L = Scalar (T)$
Assertion	lmhmlem	$⊢ F \in (S LMHom T) \to ((S \in LMod \land T \in LMod) \land (F \in (S GrpHom T) \land L = K))$

Step	Hyp	Ref	Expression
1		lmhmlem.k	$⊢ K = Scalar (S)$
2		lmhmlem.l	$⊢ L = Scalar (T)$
3		eqid	$⊢ {Base}_{K} = {Base}_{K}$
4		eqid	$⊢ {Base}_{S} = {Base}_{S}$
5		eqid	$⊢ \cdot_{S} = \cdot_{S}$
6		eqid	$⊢ \cdot_{T} = \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 a \in {Base}_{K} \forall b \in {Base}_{S} F (a \cdot_{S} b) = a \cdot_{T} F (b)))$
8		3simpa	$⊢ (F \in (S GrpHom T) \land L = K \land \forall a \in {Base}_{K} \forall b \in {Base}_{S} F (a \cdot_{S} b) = a \cdot_{T} F (b)) \to (F \in (S GrpHom T) \land L = K)$
9	8	anim2i	$⊢ ((S \in LMod \land T \in LMod) \land (F \in (S GrpHom T) \land L = K \land \forall a \in {Base}_{K} \forall b \in {Base}_{S} F (a \cdot_{S} b) = a \cdot_{T} F (b))) \to ((S \in LMod \land T \in LMod) \land (F \in (S GrpHom T) \land L = K))$
10	7 9	sylbi	$⊢ F \in (S LMHom T) \to ((S \in LMod \land T \in LMod) \land (F \in (S GrpHom T) \land L = K))$

Metamath Proof Explorer