gicref

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

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

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

Metamath Proof Explorer