Metamath Proof Explorer

Theorem gicref

Description: Isomorphism is reflexive. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Assertion gicref 
|- ( R e. Grp -> R ~=g R )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` R ) = ( Base ` R )
2 1 idghm 
 |-  ( R e. Grp -> ( _I |` ( Base ` R ) ) e. ( R GrpHom R ) )
3 cnvresid 
 |-  `' ( _I |` ( Base ` R ) ) = ( _I |` ( Base ` R ) )
4 3 2 eqeltrid 
 |-  ( R e. Grp -> `' ( _I |` ( Base ` R ) ) e. ( R GrpHom R ) )
5 isgim2 
 |-  ( ( _I |` ( Base ` R ) ) e. ( R GrpIso R ) <-> ( ( _I |` ( Base ` R ) ) e. ( R GrpHom R ) /\ `' ( _I |` ( Base ` R ) ) e. ( R GrpHom R ) ) )
6 2 4 5 sylanbrc 
 |-  ( R e. Grp -> ( _I |` ( Base ` R ) ) e. ( R GrpIso R ) )
7 brgici 
 |-  ( ( _I |` ( Base ` R ) ) e. ( R GrpIso R ) -> R ~=g R )
8 6 7 syl 
 |-  ( R e. Grp -> R ~=g R )