Theorem ricref

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

	Ref	Expression
Assertion	ricref	⊢ ( 𝑅 ∈ Ring → 𝑅 ≃𝑟 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
2	1	idrhm	⊢ ( 𝑅 ∈ Ring → ( I ↾ ( Base ‘ 𝑅 ) ) ∈ ( 𝑅 RingHom 𝑅 ) )
3		f1oi	⊢ ( I ↾ ( Base ‘ 𝑅 ) ) : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑅 )
4	1 1	isrim	⊢ ( ( I ↾ ( Base ‘ 𝑅 ) ) ∈ ( 𝑅 RingIso 𝑅 ) ↔ ( ( I ↾ ( Base ‘ 𝑅 ) ) ∈ ( 𝑅 RingHom 𝑅 ) ∧ ( I ↾ ( Base ‘ 𝑅 ) ) : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑅 ) ) )
5	2 3 4	sylanblrc	⊢ ( 𝑅 ∈ Ring → ( I ↾ ( Base ‘ 𝑅 ) ) ∈ ( 𝑅 RingIso 𝑅 ) )
6		brrici	⊢ ( ( I ↾ ( Base ‘ 𝑅 ) ) ∈ ( 𝑅 RingIso 𝑅 ) → 𝑅 ≃𝑟 𝑅 )
7	5 6	syl	⊢ ( 𝑅 ∈ Ring → 𝑅 ≃𝑟 𝑅 )