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

Metamath Proof Explorer

Theorem rhmeql

Description: The equalizer of two ring homomorphisms is a subring. (Contributed by Stefan O'Rear, 7-Mar-2015) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Assertion rhmeql ( ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubRing ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 rhmghm ⊢ ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
2 rhmghm ⊢ ( 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) → 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) )
3 ghmeql ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubGrp ‘ 𝑆 ) )
4 1 2 3 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubGrp ‘ 𝑆 ) )
5 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
6 eqid ⊢ ( mulGrp ‘ 𝑇 ) = ( mulGrp ‘ 𝑇 )
7 5 6 rhmmhm ⊢ ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) )
8 5 6 rhmmhm ⊢ ( 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) → 𝐺 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) )
9 mhmeql ⊢ ( ( 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) ∧ 𝐺 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑆 ) ) )
10 7 8 9 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑆 ) ) )
11 rhmrcl1 ⊢ ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) → 𝑆 ∈ Ring )
12 11 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) ) → 𝑆 ∈ Ring )
13 5 issubrg3 ⊢ ( 𝑆 ∈ Ring → ( dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubRing ‘ 𝑆 ) ↔ ( dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubGrp ‘ 𝑆 ) ∧ dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑆 ) ) ) ) )
14 12 13 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) ) → ( dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubRing ‘ 𝑆 ) ↔ ( dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubGrp ‘ 𝑆 ) ∧ dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑆 ) ) ) ) )
15 4 10 14 mpbir2and ⊢ ( ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 RingHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubRing ‘ 𝑆 ) )