gimco

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

		Ref	Expression
	Assertion	gimco	$⊢ (F \in (T GrpIso U) \land G \in (S GrpIso T)) \to F \circ G \in (S GrpIso U)$

Step	Hyp	Ref	Expression
1		isgim2	$⊢ F \in (T GrpIso U) \leftrightarrow (F \in (T GrpHom U) \land F^{-1} \in (U GrpHom T))$
2		isgim2	$⊢ G \in (S GrpIso T) \leftrightarrow (G \in (S GrpHom T) \land G^{-1} \in (T GrpHom S))$
3		ghmco	$⊢ (F \in (T GrpHom U) \land G \in (S GrpHom T)) \to F \circ G \in (S GrpHom U)$
4		cnvco	$⊢ {(F \circ G)}^{-1} = G^{-1} \circ F^{-1}$
5		ghmco	$⊢ (G^{-1} \in (T GrpHom S) \land F^{-1} \in (U GrpHom T)) \to G^{-1} \circ F^{-1} \in (U GrpHom S)$
6	5	ancoms	$⊢ (F^{-1} \in (U GrpHom T) \land G^{-1} \in (T GrpHom S)) \to G^{-1} \circ F^{-1} \in (U GrpHom S)$
7	4 6	eqeltrid	$⊢ (F^{-1} \in (U GrpHom T) \land G^{-1} \in (T GrpHom S)) \to {(F \circ G)}^{-1} \in (U GrpHom S)$
8	3 7	anim12i	$⊢ ((F \in (T GrpHom U) \land G \in (S GrpHom T)) \land (F^{-1} \in (U GrpHom T) \land G^{-1} \in (T GrpHom S))) \to (F \circ G \in (S GrpHom U) \land {(F \circ G)}^{-1} \in (U GrpHom S))$
9	8	an4s	$⊢ ((F \in (T GrpHom U) \land F^{-1} \in (U GrpHom T)) \land (G \in (S GrpHom T) \land G^{-1} \in (T GrpHom S))) \to (F \circ G \in (S GrpHom U) \land {(F \circ G)}^{-1} \in (U GrpHom S))$
10	1 2 9	syl2anb	$⊢ (F \in (T GrpIso U) \land G \in (S GrpIso T)) \to (F \circ G \in (S GrpHom U) \land {(F \circ G)}^{-1} \in (U GrpHom S))$
11		isgim2	$⊢ F \circ G \in (S GrpIso U) \leftrightarrow (F \circ G \in (S GrpHom U) \land {(F \circ G)}^{-1} \in (U GrpHom S))$
12	10 11	sylibr	$⊢ (F \in (T GrpIso U) \land G \in (S GrpIso T)) \to F \circ G \in (S GrpIso U)$

Metamath Proof Explorer