rhmisrnghm

Description: Each unital ring homomorphism is a non-unital ring homomorphism. (Contributed by AV, 29-Feb-2020)

		Ref	Expression
	Assertion	rhmisrnghm	$⊢ F \in (R RingHom S) \to F \in (R RngHomo S)$

Step	Hyp	Ref	Expression
1		ringrng	$⊢ R \in Ring \to R \in Rng$
2		ringrng	$⊢ S \in Ring \to S \in Rng$
3	1 2	anim12i	$⊢ (R \in Ring \land S \in Ring) \to (R \in Rng \land S \in Rng)$
4		mhmismgmhm	$⊢ F \in ({mulGrp}_{R} MndHom {mulGrp}_{S}) \to F \in ({mulGrp}_{R} MgmHom {mulGrp}_{S})$
5	4	anim2i	$⊢ (F \in (R GrpHom S) \land F \in ({mulGrp}_{R} MndHom {mulGrp}_{S})) \to (F \in (R GrpHom S) \land F \in ({mulGrp}_{R} MgmHom {mulGrp}_{S}))$
6	3 5	anim12i	$⊢ ((R \in Ring \land S \in Ring) \land (F \in (R GrpHom S) \land F \in ({mulGrp}_{R} MndHom {mulGrp}_{S}))) \to ((R \in Rng \land S \in Rng) \land (F \in (R GrpHom S) \land F \in ({mulGrp}_{R} MgmHom {mulGrp}_{S})))$
7		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
8		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
9	7 8	isrhm	$⊢ F \in (R RingHom S) \leftrightarrow ((R \in Ring \land S \in Ring) \land (F \in (R GrpHom S) \land F \in ({mulGrp}_{R} MndHom {mulGrp}_{S})))$
10	7 8	isrnghmmul	$⊢ F \in (R RngHomo S) \leftrightarrow ((R \in Rng \land S \in Rng) \land (F \in (R GrpHom S) \land F \in ({mulGrp}_{R} MgmHom {mulGrp}_{S})))$
11	6 9 10	3imtr4i	$⊢ F \in (R RingHom S) \to F \in (R RngHomo S)$

Metamath Proof Explorer