Metamath Proof Explorer


Theorem gicref

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

Ref Expression
Assertion gicref ( 𝑅 ∈ Grp → 𝑅𝑔 𝑅 )

Proof

Step Hyp Ref Expression
1 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
2 1 idghm ( 𝑅 ∈ Grp → ( I ↾ ( Base ‘ 𝑅 ) ) ∈ ( 𝑅 GrpHom 𝑅 ) )
3 cnvresid ( I ↾ ( Base ‘ 𝑅 ) ) = ( I ↾ ( Base ‘ 𝑅 ) )
4 3 2 eqeltrid ( 𝑅 ∈ Grp → ( I ↾ ( Base ‘ 𝑅 ) ) ∈ ( 𝑅 GrpHom 𝑅 ) )
5 isgim2 ( ( I ↾ ( Base ‘ 𝑅 ) ) ∈ ( 𝑅 GrpIso 𝑅 ) ↔ ( ( I ↾ ( Base ‘ 𝑅 ) ) ∈ ( 𝑅 GrpHom 𝑅 ) ∧ ( I ↾ ( Base ‘ 𝑅 ) ) ∈ ( 𝑅 GrpHom 𝑅 ) ) )
6 2 4 5 sylanbrc ( 𝑅 ∈ Grp → ( I ↾ ( Base ‘ 𝑅 ) ) ∈ ( 𝑅 GrpIso 𝑅 ) )
7 brgici ( ( I ↾ ( Base ‘ 𝑅 ) ) ∈ ( 𝑅 GrpIso 𝑅 ) → 𝑅𝑔 𝑅 )
8 6 7 syl ( 𝑅 ∈ Grp → 𝑅𝑔 𝑅 )