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 ( ( 𝐹 ∈ ( 𝑇 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 𝑈 ) )