Metamath Proof Explorer

Theorem ricref

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

Ref Expression
Assertion ricref 
|- ( R e. Ring -> R ~=r R )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` R ) = ( Base ` R )
2 1 idrhm 
 |-  ( R e. Ring -> ( _I |` ( Base ` R ) ) e. ( R RingHom R ) )
3 f1oi 
 |-  ( _I |` ( Base ` R ) ) : ( Base ` R ) -1-1-onto-> ( Base ` R )
4 1 1 isrim 
 |-  ( ( _I |` ( Base ` R ) ) e. ( R RingIso R ) <-> ( ( _I |` ( Base ` R ) ) e. ( R RingHom R ) /\ ( _I |` ( Base ` R ) ) : ( Base ` R ) -1-1-onto-> ( Base ` R ) ) )
5 2 3 4 sylanblrc 
 |-  ( R e. Ring -> ( _I |` ( Base ` R ) ) e. ( R RingIso R ) )
6 brrici 
 |-  ( ( _I |` ( Base ` R ) ) e. ( R RingIso R ) -> R ~=r R )
7 5 6 syl 
 |-  ( R e. Ring -> R ~=r R )