This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 → 𝑅 ≃𝑔 𝑅 )