rnghmval2

Description: The non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 1-Mar-2020)

		Ref	Expression
	Assertion	rnghmval2	$⊢ (R \in Rng \land S \in Rng) \to R RngHomo S = (R GrpHom S) \cap ({mulGrp}_{R} MgmHom {mulGrp}_{S})$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
2		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
3	1 2	isrnghmmul	$⊢ h \in (R RngHomo S) \leftrightarrow ((R \in Rng \land S \in Rng) \land (h \in (R GrpHom S) \land h \in ({mulGrp}_{R} MgmHom {mulGrp}_{S})))$
4		elin	$⊢ h \in ((R GrpHom S) \cap ({mulGrp}_{R} MgmHom {mulGrp}_{S})) \leftrightarrow (h \in (R GrpHom S) \land h \in ({mulGrp}_{R} MgmHom {mulGrp}_{S}))$
5		ibar	$⊢ (R \in Rng \land S \in Rng) \to ((h \in (R GrpHom S) \land h \in ({mulGrp}_{R} MgmHom {mulGrp}_{S})) \leftrightarrow ((R \in Rng \land S \in Rng) \land (h \in (R GrpHom S) \land h \in ({mulGrp}_{R} MgmHom {mulGrp}_{S}))))$
6	4 5	bitr2id	$⊢ (R \in Rng \land S \in Rng) \to (((R \in Rng \land S \in Rng) \land (h \in (R GrpHom S) \land h \in ({mulGrp}_{R} MgmHom {mulGrp}_{S}))) \leftrightarrow h \in ((R GrpHom S) \cap ({mulGrp}_{R} MgmHom {mulGrp}_{S})))$
7	3 6	syl5bb	$⊢ (R \in Rng \land S \in Rng) \to (h \in (R RngHomo S) \leftrightarrow h \in ((R GrpHom S) \cap ({mulGrp}_{R} MgmHom {mulGrp}_{S})))$
8	7	eqrdv	$⊢ (R \in Rng \land S \in Rng) \to R RngHomo S = (R GrpHom S) \cap ({mulGrp}_{R} MgmHom {mulGrp}_{S})$

Metamath Proof Explorer