Metamath Proof Explorer

Theorem rhmco

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

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

Proof

Step Hyp Ref Expression
1 rhmrcl2 
 |-  ( F e. ( T RingHom U ) -> U e. Ring )
2 rhmrcl1 
 |-  ( G e. ( S RingHom T ) -> S e. Ring )
3 1 2 anim12ci 
 |-  ( ( F e. ( T RingHom U ) /\ G e. ( S RingHom T ) ) -> ( S e. Ring /\ U e. Ring ) )
4 rhmghm 
 |-  ( F e. ( T RingHom U ) -> F e. ( T GrpHom U ) )
5 rhmghm 
 |-  ( G e. ( S RingHom T ) -> G e. ( S GrpHom T ) )
6 ghmco 
 |-  ( ( F e. ( T GrpHom U ) /\ G e. ( S GrpHom T ) ) -> ( F o. G ) e. ( S GrpHom U ) )
7 4 5 6 syl2an 
 |-  ( ( F e. ( T RingHom U ) /\ G e. ( S RingHom T ) ) -> ( F o. G ) e. ( S GrpHom U ) )
8 eqid 
 |-  ( mulGrp ` T ) = ( mulGrp ` T )
9 eqid 
 |-  ( mulGrp ` U ) = ( mulGrp ` U )
10 8 9 rhmmhm 
 |-  ( F e. ( T RingHom U ) -> F e. ( ( mulGrp ` T ) MndHom ( mulGrp ` U ) ) )
11 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
12 11 8 rhmmhm 
 |-  ( G e. ( S RingHom T ) -> G e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) )
13 mhmco 
 |-  ( ( F e. ( ( mulGrp ` T ) MndHom ( mulGrp ` U ) ) /\ G e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) ) -> ( F o. G ) e. ( ( mulGrp ` S ) MndHom ( mulGrp ` U ) ) )
14 10 12 13 syl2an 
 |-  ( ( F e. ( T RingHom U ) /\ G e. ( S RingHom T ) ) -> ( F o. G ) e. ( ( mulGrp ` S ) MndHom ( mulGrp ` U ) ) )
15 7 14 jca 
 |-  ( ( F e. ( T RingHom U ) /\ G e. ( S RingHom T ) ) -> ( ( F o. G ) e. ( S GrpHom U ) /\ ( F o. G ) e. ( ( mulGrp ` S ) MndHom ( mulGrp ` U ) ) ) )
16 11 9 isrhm 
 |-  ( ( F o. G ) e. ( S RingHom U ) <-> ( ( S e. Ring /\ U e. Ring ) /\ ( ( F o. G ) e. ( S GrpHom U ) /\ ( F o. G ) e. ( ( mulGrp ` S ) MndHom ( mulGrp ` U ) ) ) ) )
17 3 15 16 sylanbrc 
 |-  ( ( F e. ( T RingHom U ) /\ G e. ( S RingHom T ) ) -> ( F o. G ) e. ( S RingHom U ) )