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 ( ( 𝐹 ∈ ( 𝑇 RngHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 RngHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 RngHom 𝑈 ) )

Proof

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