Metamath Proof Explorer


Theorem gicref

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

Ref Expression
Assertion gicref RGrpR𝑔R

Proof

Step Hyp Ref Expression
1 eqid BaseR=BaseR
2 1 idghm RGrpIBaseRRGrpHomR
3 cnvresid IBaseR-1=IBaseR
4 3 2 eqeltrid RGrpIBaseR-1RGrpHomR
5 isgim2 IBaseRRGrpIsoRIBaseRRGrpHomRIBaseR-1RGrpHomR
6 2 4 5 sylanbrc RGrpIBaseRRGrpIsoR
7 brgici IBaseRRGrpIsoRR𝑔R
8 6 7 syl RGrpR𝑔R