rimisrngim

Description: Each unital ring isomorphism is a non-unital ring isomorphism. (Contributed by AV, 30-Mar-2025)

		Ref	Expression
	Assertion	rimisrngim	$⊢ F \in (R RingIso S) \to F \in (R RngIso S)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{R} = {Base}_{R}$
2		eqid	$⊢ {Base}_{S} = {Base}_{S}$
3	1 2	isrim	$⊢ F \in (R RingIso S) \leftrightarrow (F \in (R RingHom S) \land F : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S})$
4		rhmisrnghm	$⊢ F \in (R RingHom S) \to F \in (R RngHom S)$
5	4	anim1i	$⊢ (F \in (R RingHom S) \land F : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S}) \to (F \in (R RngHom S) \land F : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S})$
6	3 5	sylbi	$⊢ F \in (R RingIso S) \to (F \in (R RngHom S) \land F : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S})$
7		rimrcl	$⊢ F \in (R RingIso S) \to (R \in V \land S \in V)$
8	1 2	isrngim2	$⊢ (R \in V \land S \in V) \to (F \in (R RngIso S) \leftrightarrow (F \in (R RngHom S) \land F : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S}))$
9	7 8	syl	$⊢ F \in (R RingIso S) \to (F \in (R RngIso S) \leftrightarrow (F \in (R RngHom S) \land F : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S}))$
10	6 9	mpbird	$⊢ F \in (R RingIso S) \to F \in (R RngIso S)$

Metamath Proof Explorer