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

Metamath Proof Explorer

Theorem isgim2

Description: A group isomorphism is a homomorphism whose converse is also a homomorphism. Characterization of isomorphisms similar to ishmeo . (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Assertion isgim2 ⊢ F ∈ R GrpIso S ↔ F ∈ R GrpHom S ∧ F -1 ∈ S GrpHom R

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base R = Base R
2 eqid ⊢ Base S = Base S
3 1 2 isgim ⊢ F ∈ R GrpIso S ↔ F ∈ R GrpHom S ∧ F : Base R ⟶ 1-1 onto Base S
4 1 2 ghmf1o ⊢ F ∈ R GrpHom S → F : Base R ⟶ 1-1 onto Base S ↔ F -1 ∈ S GrpHom R
5 4 pm5.32i ⊢ F ∈ R GrpHom S ∧ F : Base R ⟶ 1-1 onto Base S ↔ F ∈ R GrpHom S ∧ F -1 ∈ S GrpHom R
6 3 5 bitri ⊢ F ∈ R GrpIso S ↔ F ∈ R GrpHom S ∧ F -1 ∈ S GrpHom R