rhmco

Description: The composition of ring homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015)

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

Step	Hyp	Ref	Expression
1		rhmrcl2	$⊢ F \in (T RingHom U) \to U \in Ring$
2		rhmrcl1	$⊢ G \in (S RingHom T) \to S \in Ring$
3	1 2	anim12ci	$⊢ (F \in (T RingHom U) \land G \in (S RingHom T)) \to (S \in Ring \land U \in Ring)$
4		rhmghm	$⊢ F \in (T RingHom U) \to F \in (T GrpHom U)$
5		rhmghm	$⊢ G \in (S RingHom T) \to G \in (S GrpHom T)$
6		ghmco	$⊢ (F \in (T GrpHom U) \land G \in (S GrpHom T)) \to F \circ G \in (S GrpHom U)$
7	4 5 6	syl2an	$⊢ (F \in (T RingHom U) \land G \in (S RingHom T)) \to F \circ G \in (S GrpHom U)$
8		eqid	$⊢ {mulGrp}_{T} = {mulGrp}_{T}$
9		eqid	$⊢ {mulGrp}_{U} = {mulGrp}_{U}$
10	8 9	rhmmhm	$⊢ F \in (T RingHom U) \to F \in ({mulGrp}_{T} MndHom {mulGrp}_{U})$
11		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
12	11 8	rhmmhm	$⊢ G \in (S RingHom T) \to G \in ({mulGrp}_{S} MndHom {mulGrp}_{T})$
13		mhmco	$⊢ (F \in ({mulGrp}_{T} MndHom {mulGrp}_{U}) \land G \in ({mulGrp}_{S} MndHom {mulGrp}_{T})) \to F \circ G \in ({mulGrp}_{S} MndHom {mulGrp}_{U})$
14	10 12 13	syl2an	$⊢ (F \in (T RingHom U) \land G \in (S RingHom T)) \to F \circ G \in ({mulGrp}_{S} MndHom {mulGrp}_{U})$
15	7 14	jca	$⊢ (F \in (T RingHom U) \land G \in (S RingHom T)) \to (F \circ G \in (S GrpHom U) \land F \circ G \in ({mulGrp}_{S} MndHom {mulGrp}_{U}))$
16	11 9	isrhm	$⊢ F \circ G \in (S RingHom U) \leftrightarrow ((S \in Ring \land U \in Ring) \land (F \circ G \in (S GrpHom U) \land F \circ G \in ({mulGrp}_{S} MndHom {mulGrp}_{U})))$
17	3 15 16	sylanbrc	$⊢ (F \in (T RingHom U) \land G \in (S RingHom T)) \to F \circ G \in (S RingHom U)$

Metamath Proof Explorer