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

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