rngimrnghm

Description: An isomorphism of non-unital rings is a homomorphism. (Contributed by AV, 23-Feb-2020)

Step	Hyp	Ref	Expression
1		rnghmf1o.b	$⊢ B = {Base}_{R}$
2		rnghmf1o.c	$⊢ C = {Base}_{S}$
3		rngimrcl	$⊢ F \in (R RngIso S) \to (R \in V \land S \in V)$
4	1 2	isrngim2	$⊢ (R \in V \land S \in V) \to (F \in (R RngIso S) \leftrightarrow (F \in (R RngHom S) \land F : B \underset{1-1 onto}{⟶} C))$
5		simpl	$⊢ (F \in (R RngHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F \in (R RngHom S)$
6	4 5	syl6bi	$⊢ (R \in V \land S \in V) \to (F \in (R RngIso S) \to F \in (R RngHom S))$
7	3 6	mpcom	$⊢ F \in (R RngIso S) \to F \in (R RngHom S)$

Metamath Proof Explorer