Metamath Proof Explorer

Theorem gimcnv

Description: The converse of a bijective group homomorphism is a bijective group homomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Assertion gimcnv ⊢ F ∈ S GrpIso T → F -1 ∈ T GrpIso S

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base S = Base S
2 eqid ⊢ Base T = Base T
3 1 2 ghmf ⊢ F ∈ S GrpHom T → F : Base S ⟶ Base T
4 frel ⊢ F : Base S ⟶ Base T → Rel ⁡ F
5 dfrel2 ⊢ Rel ⁡ F ↔ F -1 -1 = F
6 4 5 sylib ⊢ F : Base S ⟶ Base T → F -1 -1 = F
7 3 6 syl ⊢ F ∈ S GrpHom T → F -1 -1 = F
8 id ⊢ F ∈ S GrpHom T → F ∈ S GrpHom T
9 7 8 eqeltrd ⊢ F ∈ S GrpHom T → F -1 -1 ∈ S GrpHom T
10 9 anim1ci ⊢ F ∈ S GrpHom T ∧ F -1 ∈ T GrpHom S → F -1 ∈ T GrpHom S ∧ F -1 -1 ∈ S GrpHom T
11 isgim2 ⊢ F ∈ S GrpIso T ↔ F ∈ S GrpHom T ∧ F -1 ∈ T GrpHom S
12 isgim2 ⊢ F -1 ∈ T GrpIso S ↔ F -1 ∈ T GrpHom S ∧ F -1 -1 ∈ S GrpHom T
13 10 11 12 3imtr4i ⊢ F ∈ S GrpIso T → F -1 ∈ T GrpIso S