Theorem rhmco

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

	Ref	Expression
Assertion	rhmco	⊢ ( ( 𝐹 ∈ ( 𝑇 RingHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 RingHom 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		rhmrcl2	⊢ ( 𝐹 ∈ ( 𝑇 RingHom 𝑈 ) → 𝑈 ∈ Ring )
2		rhmrcl1	⊢ ( 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) → 𝑆 ∈ Ring )
3	1 2	anim12ci	⊢ ( ( 𝐹 ∈ ( 𝑇 RingHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) ) → ( 𝑆 ∈ Ring ∧ 𝑈 ∈ Ring ) )
4		rhmghm	⊢ ( 𝐹 ∈ ( 𝑇 RingHom 𝑈 ) → 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) )
5		rhmghm	⊢ ( 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) → 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) )
6		ghmco	⊢ ( ( 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GrpHom 𝑈 ) )
7	4 5 6	syl2an	⊢ ( ( 𝐹 ∈ ( 𝑇 RingHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GrpHom 𝑈 ) )
8		eqid	⊢ ( mulGrp ‘ 𝑇 ) = ( mulGrp ‘ 𝑇 )
9		eqid	⊢ ( mulGrp ‘ 𝑈 ) = ( mulGrp ‘ 𝑈 )
10	8 9	rhmmhm	⊢ ( 𝐹 ∈ ( 𝑇 RingHom 𝑈 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑇 ) MndHom ( mulGrp ‘ 𝑈 ) ) )
11		eqid	⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
12	11 8	rhmmhm	⊢ ( 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) → 𝐺 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) )
13		mhmco	⊢ ( ( 𝐹 ∈ ( ( mulGrp ‘ 𝑇 ) MndHom ( mulGrp ‘ 𝑈 ) ) ∧ 𝐺 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑈 ) ) )
14	10 12 13	syl2an	⊢ ( ( 𝐹 ∈ ( 𝑇 RingHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑈 ) ) )
15	7 14	jca	⊢ ( ( 𝐹 ∈ ( 𝑇 RingHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) ) → ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GrpHom 𝑈 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑈 ) ) ) )
16	11 9	isrhm	⊢ ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 RingHom 𝑈 ) ↔ ( ( 𝑆 ∈ Ring ∧ 𝑈 ∈ Ring ) ∧ ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GrpHom 𝑈 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑈 ) ) ) ) )
17	3 15 16	sylanbrc	⊢ ( ( 𝐹 ∈ ( 𝑇 RingHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 RingHom 𝑈 ) )