rngimrnghm

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

	Ref	Expression
Hypotheses	rnghmf1o.b	$⊢ B = {Base}_{R}$
	rnghmf1o.c	$⊢ C = {Base}_{S}$
Assertion	rngimrnghm	$⊢ F \in (R RngIsom S) \to F \in (R RngHomo S)$

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

Metamath Proof Explorer