Theorem rnghmco

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

	Ref	Expression
Assertion	rnghmco	|- ( ( F e. ( T RngHom U ) /\ G e. ( S RngHom T ) ) -> ( F o. G ) e. ( S RngHom U ) )

Proof

Step	Hyp	Ref	Expression
1		rnghmrcl	|- ( F e. ( T RngHom U ) -> ( T e. Rng /\ U e. Rng ) )
2	1	simprd	|- ( F e. ( T RngHom U ) -> U e. Rng )
3		rnghmrcl	|- ( G e. ( S RngHom T ) -> ( S e. Rng /\ T e. Rng ) )
4	3	simpld	|- ( G e. ( S RngHom T ) -> S e. Rng )
5	2 4	anim12ci	|- ( ( F e. ( T RngHom U ) /\ G e. ( S RngHom T ) ) -> ( S e. Rng /\ U e. Rng ) )
6		rnghmghm	|- ( F e. ( T RngHom U ) -> F e. ( T GrpHom U ) )
7		rnghmghm	|- ( G e. ( S RngHom T ) -> G e. ( S GrpHom T ) )
8		ghmco	|- ( ( F e. ( T GrpHom U ) /\ G e. ( S GrpHom T ) ) -> ( F o. G ) e. ( S GrpHom U ) )
9	6 7 8	syl2an	|- ( ( F e. ( T RngHom U ) /\ G e. ( S RngHom T ) ) -> ( F o. G ) e. ( S GrpHom U ) )
10		eqid	|- ( mulGrp ` T ) = ( mulGrp ` T )
11		eqid	|- ( mulGrp ` U ) = ( mulGrp ` U )
12	10 11	rnghmmgmhm	|- ( F e. ( T RngHom U ) -> F e. ( ( mulGrp ` T ) MgmHom ( mulGrp ` U ) ) )
13		eqid	|- ( mulGrp ` S ) = ( mulGrp ` S )
14	13 10	rnghmmgmhm	|- ( G e. ( S RngHom T ) -> G e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` T ) ) )
15		mgmhmco	|- ( ( F e. ( ( mulGrp ` T ) MgmHom ( mulGrp ` U ) ) /\ G e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` T ) ) ) -> ( F o. G ) e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` U ) ) )
16	12 14 15	syl2an	|- ( ( F e. ( T RngHom U ) /\ G e. ( S RngHom T ) ) -> ( F o. G ) e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` U ) ) )
17	9 16	jca	|- ( ( F e. ( T RngHom U ) /\ G e. ( S RngHom T ) ) -> ( ( F o. G ) e. ( S GrpHom U ) /\ ( F o. G ) e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` U ) ) ) )
18	13 11	isrnghmmul	|- ( ( F o. G ) e. ( S RngHom U ) <-> ( ( S e. Rng /\ U e. Rng ) /\ ( ( F o. G ) e. ( S GrpHom U ) /\ ( F o. G ) e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` U ) ) ) ) )
19	5 17 18	sylanbrc	|- ( ( F e. ( T RngHom U ) /\ G e. ( S RngHom T ) ) -> ( F o. G ) e. ( S RngHom U ) )