Theorem ricref

Description: Ring isomorphism is reflexive. (Contributed by by AV, 24-Jul-2026)

	Ref	Expression
Assertion	ricref	$$⊢R\in \mathrm{Ring}\to R{\simeq }_{𝑟}R$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
2	1	idrhm	$$⊢R\in \mathrm{Ring}\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}\in \left(R\mathrm{RingHom}R\right)$$
3		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}\right):{\mathrm{Base}}_R\underset{1-1\; onto}{⟶}{\mathrm{Base}}_R$$
4	1 1	isrim	$$⊢{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}\in \left(R\mathrm{RingIso}R\right)\leftrightarrow \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}\in \left(R\mathrm{RingHom}R\right)\wedge \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}\right):{\mathrm{Base}}_R\underset{1-1\; onto}{⟶}{\mathrm{Base}}_R\right)$$
5	2 3 4	sylanblrc	$$⊢R\in \mathrm{Ring}\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}\in \left(R\mathrm{RingIso}R\right)$$
6		brrici	$$⊢{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}\in \left(R\mathrm{RingIso}R\right)\to R{\simeq }_{𝑟}R$$
7	5 6	syl	$$⊢R\in \mathrm{Ring}\to R{\simeq }_{𝑟}R$$