Metamath Proof Explorer

Theorem gimco

Description: The composition of group isomorphisms is a group isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Assertion gimco ⊢ F ∈ T GrpIso U ∧ G ∈ S GrpIso T → F ∘ G ∈ S GrpIso U

Proof

Step Hyp Ref Expression
1 isgim2 ⊢ F ∈ T GrpIso U ↔ F ∈ T GrpHom U ∧ F -1 ∈ U GrpHom T
2 isgim2 ⊢ G ∈ S GrpIso T ↔ G ∈ S GrpHom T ∧ G -1 ∈ T GrpHom S
3 ghmco ⊢ F ∈ T GrpHom U ∧ G ∈ S GrpHom T → F ∘ G ∈ S GrpHom U
4 cnvco ⊢ F ∘ G -1 = G -1 ∘ F -1
5 ghmco ⊢ G -1 ∈ T GrpHom S ∧ F -1 ∈ U GrpHom T → G -1 ∘ F -1 ∈ U GrpHom S
6 5 ancoms ⊢ F -1 ∈ U GrpHom T ∧ G -1 ∈ T GrpHom S → G -1 ∘ F -1 ∈ U GrpHom S
7 4 6 eqeltrid ⊢ F -1 ∈ U GrpHom T ∧ G -1 ∈ T GrpHom S → F ∘ G -1 ∈ U GrpHom S
8 3 7 anim12i ⊢ F ∈ T GrpHom U ∧ G ∈ S GrpHom T ∧ F -1 ∈ U GrpHom T ∧ G -1 ∈ T GrpHom S → F ∘ G ∈ S GrpHom U ∧ F ∘ G -1 ∈ U GrpHom S
9 8 an4s ⊢ F ∈ T GrpHom U ∧ F -1 ∈ U GrpHom T ∧ G ∈ S GrpHom T ∧ G -1 ∈ T GrpHom S → F ∘ G ∈ S GrpHom U ∧ F ∘ G -1 ∈ U GrpHom S
10 1 2 9 syl2anb ⊢ F ∈ T GrpIso U ∧ G ∈ S GrpIso T → F ∘ G ∈ S GrpHom U ∧ F ∘ G -1 ∈ U GrpHom S
11 isgim2 ⊢ F ∘ G ∈ S GrpIso U ↔ F ∘ G ∈ S GrpHom U ∧ F ∘ G -1 ∈ U GrpHom S
12 10 11 sylibr ⊢ F ∈ T GrpIso U ∧ G ∈ S GrpIso T → F ∘ G ∈ S GrpIso U