This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) )