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 ⊢ F ∈ S RingHom T ∧ G ∈ S RingHom T → dom ⁡ F ∩ G ∈ SubRing ⁡ S

Proof

Step Hyp Ref Expression
1 rhmghm ⊢ F ∈ S RingHom T → F ∈ S GrpHom T
2 rhmghm ⊢ G ∈ S RingHom T → G ∈ S GrpHom T
3 ghmeql ⊢ F ∈ S GrpHom T ∧ G ∈ S GrpHom T → dom ⁡ F ∩ G ∈ SubGrp ⁡ S
4 1 2 3 syl2an ⊢ F ∈ S RingHom T ∧ G ∈ S RingHom T → dom ⁡ F ∩ G ∈ SubGrp ⁡ S
5 eqid ⊢ mulGrp S = mulGrp S
6 eqid ⊢ mulGrp T = mulGrp T
7 5 6 rhmmhm ⊢ F ∈ S RingHom T → F ∈ mulGrp S MndHom mulGrp T
8 5 6 rhmmhm ⊢ G ∈ S RingHom T → G ∈ mulGrp S MndHom mulGrp T
9 mhmeql ⊢ F ∈ mulGrp S MndHom mulGrp T ∧ G ∈ mulGrp S MndHom mulGrp T → dom ⁡ F ∩ G ∈ SubMnd ⁡ mulGrp S
10 7 8 9 syl2an ⊢ F ∈ S RingHom T ∧ G ∈ S RingHom T → dom ⁡ F ∩ G ∈ SubMnd ⁡ mulGrp S
11 rhmrcl1 ⊢ F ∈ S RingHom T → S ∈ Ring
12 11 adantr ⊢ F ∈ S RingHom T ∧ G ∈ S RingHom T → S ∈ Ring
13 5 issubrg3 ⊢ S ∈ Ring → dom ⁡ F ∩ G ∈ SubRing ⁡ S ↔ dom ⁡ F ∩ G ∈ SubGrp ⁡ S ∧ dom ⁡ F ∩ G ∈ SubMnd ⁡ mulGrp S
14 12 13 syl ⊢ F ∈ S RingHom T ∧ G ∈ S RingHom T → dom ⁡ F ∩ G ∈ SubRing ⁡ S ↔ dom ⁡ F ∩ G ∈ SubGrp ⁡ S ∧ dom ⁡ F ∩ G ∈ SubMnd ⁡ mulGrp S
15 4 10 14 mpbir2and ⊢ F ∈ S RingHom T ∧ G ∈ S RingHom T → dom ⁡ F ∩ G ∈ SubRing ⁡ S