Theorem rnghmco

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

	Ref	Expression
Assertion	rnghmco	⊢ ( ( 𝐹 ∈ ( 𝑇 RngHomo 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 RngHomo 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 RngHomo 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		rnghmrcl	⊢ ( 𝐹 ∈ ( 𝑇 RngHomo 𝑈 ) → ( 𝑇 ∈ Rng ∧ 𝑈 ∈ Rng ) )
2	1	simprd	⊢ ( 𝐹 ∈ ( 𝑇 RngHomo 𝑈 ) → 𝑈 ∈ Rng )
3		rnghmrcl	⊢ ( 𝐺 ∈ ( 𝑆 RngHomo 𝑇 ) → ( 𝑆 ∈ Rng ∧ 𝑇 ∈ Rng ) )
4	3	simpld	⊢ ( 𝐺 ∈ ( 𝑆 RngHomo 𝑇 ) → 𝑆 ∈ Rng )
5	2 4	anim12ci	⊢ ( ( 𝐹 ∈ ( 𝑇 RngHomo 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 RngHomo 𝑇 ) ) → ( 𝑆 ∈ Rng ∧ 𝑈 ∈ Rng ) )
6		rnghmghm	⊢ ( 𝐹 ∈ ( 𝑇 RngHomo 𝑈 ) → 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) )
7		rnghmghm	⊢ ( 𝐺 ∈ ( 𝑆 RngHomo 𝑇 ) → 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) )
8		ghmco	⊢ ( ( 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GrpHom 𝑈 ) )
9	6 7 8	syl2an	⊢ ( ( 𝐹 ∈ ( 𝑇 RngHomo 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 RngHomo 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GrpHom 𝑈 ) )
10		eqid	⊢ ( mulGrp ‘ 𝑇 ) = ( mulGrp ‘ 𝑇 )
11		eqid	⊢ ( mulGrp ‘ 𝑈 ) = ( mulGrp ‘ 𝑈 )
12	10 11	rnghmmgmhm	⊢ ( 𝐹 ∈ ( 𝑇 RngHomo 𝑈 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑇 ) MgmHom ( mulGrp ‘ 𝑈 ) ) )
13		eqid	⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
14	13 10	rnghmmgmhm	⊢ ( 𝐺 ∈ ( 𝑆 RngHomo 𝑇 ) → 𝐺 ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑇 ) ) )
15		mgmhmco	⊢ ( ( 𝐹 ∈ ( ( mulGrp ‘ 𝑇 ) MgmHom ( mulGrp ‘ 𝑈 ) ) ∧ 𝐺 ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑇 ) ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑈 ) ) )
16	12 14 15	syl2an	⊢ ( ( 𝐹 ∈ ( 𝑇 RngHomo 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 RngHomo 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑈 ) ) )
17	9 16	jca	⊢ ( ( 𝐹 ∈ ( 𝑇 RngHomo 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 RngHomo 𝑇 ) ) → ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GrpHom 𝑈 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑈 ) ) ) )
18	13 11	isrnghmmul	⊢ ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 RngHomo 𝑈 ) ↔ ( ( 𝑆 ∈ Rng ∧ 𝑈 ∈ Rng ) ∧ ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GrpHom 𝑈 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑈 ) ) ) ) )
19	5 17 18	sylanbrc	⊢ ( ( 𝐹 ∈ ( 𝑇 RngHomo 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 RngHomo 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 RngHomo 𝑈 ) )