Theorem gicref

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

	Ref	Expression
Assertion	gicref	$$⊢R\in \mathrm{Grp}\to R{\simeq }_{𝑔}R$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
2	1	idghm	$$⊢R\in \mathrm{Grp}\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}\in \left(R\mathrm{GrpHom}R\right)$$
3		cnvresid	$$⊢{\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}\right)}^{-1}={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}$$
4	3 2	eqeltrid	$$⊢R\in \mathrm{Grp}\to {\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}\right)}^{-1}\in \left(R\mathrm{GrpHom}R\right)$$
5		isgim2	$$⊢{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}\in \left(R\mathrm{GrpIso}R\right)\leftrightarrow \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}\in \left(R\mathrm{GrpHom}R\right)\wedge {\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}\right)}^{-1}\in \left(R\mathrm{GrpHom}R\right)\right)$$
6	2 4 5	sylanbrc	$$⊢R\in \mathrm{Grp}\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}\in \left(R\mathrm{GrpIso}R\right)$$
7		brgici	$$⊢{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_R}\in \left(R\mathrm{GrpIso}R\right)\to R{\simeq }_{𝑔}R$$
8	6 7	syl	$$⊢R\in \mathrm{Grp}\to R{\simeq }_{𝑔}R$$