Metamath Proof Explorer

Theorem rnghmco

Description: The composition of non-unital ring homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020)

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

Proof

Step	Hyp	Ref	Expression
1		rnghmrcl	$⊢ F \in (T RngHom U) \to (T \in Rng \land U \in Rng)$
2	1	simprd	$⊢ F \in (T RngHom U) \to U \in Rng$
3		rnghmrcl	$⊢ G \in (S RngHom T) \to (S \in Rng \land T \in Rng)$
4	3	simpld	$⊢ G \in (S RngHom T) \to S \in Rng$
5	2 4	anim12ci	$⊢ (F \in (T RngHom U) \land G \in (S RngHom T)) \to (S \in Rng \land U \in Rng)$
6		rnghmghm	$⊢ F \in (T RngHom U) \to F \in (T GrpHom U)$
7		rnghmghm	$⊢ G \in (S RngHom T) \to G \in (S GrpHom T)$
8		ghmco	$⊢ (F \in (T GrpHom U) \land G \in (S GrpHom T)) \to F \circ G \in (S GrpHom U)$
9	6 7 8	syl2an	$⊢ (F \in (T RngHom U) \land G \in (S RngHom T)) \to F \circ G \in (S GrpHom U)$
10		eqid	$⊢ {mulGrp}_{T} = {mulGrp}_{T}$
11		eqid	$⊢ {mulGrp}_{U} = {mulGrp}_{U}$
12	10 11	rnghmmgmhm	$⊢ F \in (T RngHom U) \to F \in ({mulGrp}_{T} MgmHom {mulGrp}_{U})$
13		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
14	13 10	rnghmmgmhm	$⊢ G \in (S RngHom T) \to G \in ({mulGrp}_{S} MgmHom {mulGrp}_{T})$
15		mgmhmco	$⊢ (F \in ({mulGrp}_{T} MgmHom {mulGrp}_{U}) \land G \in ({mulGrp}_{S} MgmHom {mulGrp}_{T})) \to F \circ G \in ({mulGrp}_{S} MgmHom {mulGrp}_{U})$
16	12 14 15	syl2an	$⊢ (F \in (T RngHom U) \land G \in (S RngHom T)) \to F \circ G \in ({mulGrp}_{S} MgmHom {mulGrp}_{U})$
17	9 16	jca	$⊢ (F \in (T RngHom U) \land G \in (S RngHom T)) \to (F \circ G \in (S GrpHom U) \land F \circ G \in ({mulGrp}_{S} MgmHom {mulGrp}_{U}))$
18	13 11	isrnghmmul	$⊢ F \circ G \in (S RngHom U) \leftrightarrow ((S \in Rng \land U \in Rng) \land (F \circ G \in (S GrpHom U) \land F \circ G \in ({mulGrp}_{S} MgmHom {mulGrp}_{U})))$
19	5 17 18	sylanbrc	$⊢ (F \in (T RngHom U) \land G \in (S RngHom T)) \to F \circ G \in (S RngHom U)$