rimrhm

Description: An isomorphism of rings is a homomorphism. (Contributed by AV, 22-Oct-2019)

	Ref	Expression
Hypotheses	rhmf1o.b	$⊢ B = {Base}_{R}$
	rhmf1o.c	$⊢ C = {Base}_{S}$
Assertion	rimrhm	$⊢ F \in (R RingIso S) \to F \in (R RingHom S)$

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

Metamath Proof Explorer