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 e. ( S RingHom T ) /\ G e. ( S RingHom T ) ) -> dom ( F i^i G ) e. ( SubRing ` S ) )

Proof

Step Hyp Ref Expression
1 rhmghm 
 |-  ( F e. ( S RingHom T ) -> F e. ( S GrpHom T ) )
2 rhmghm 
 |-  ( G e. ( S RingHom T ) -> G e. ( S GrpHom T ) )
3 ghmeql 
 |-  ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> dom ( F i^i G ) e. ( SubGrp ` S ) )
4 1 2 3 syl2an 
 |-  ( ( F e. ( S RingHom T ) /\ G e. ( S RingHom T ) ) -> dom ( F i^i G ) e. ( SubGrp ` S ) )
5 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
6 eqid 
 |-  ( mulGrp ` T ) = ( mulGrp ` T )
7 5 6 rhmmhm 
 |-  ( F e. ( S RingHom T ) -> F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) )
8 5 6 rhmmhm 
 |-  ( G e. ( S RingHom T ) -> G e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) )
9 mhmeql 
 |-  ( ( F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) /\ G e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) ) -> dom ( F i^i G ) e. ( SubMnd ` ( mulGrp ` S ) ) )
10 7 8 9 syl2an 
 |-  ( ( F e. ( S RingHom T ) /\ G e. ( S RingHom T ) ) -> dom ( F i^i G ) e. ( SubMnd ` ( mulGrp ` S ) ) )
11 rhmrcl1 
 |-  ( F e. ( S RingHom T ) -> S e. Ring )
12 11 adantr 
 |-  ( ( F e. ( S RingHom T ) /\ G e. ( S RingHom T ) ) -> S e. Ring )
13 5 issubrg3 
 |-  ( S e. Ring -> ( dom ( F i^i G ) e. ( SubRing ` S ) <-> ( dom ( F i^i G ) e. ( SubGrp ` S ) /\ dom ( F i^i G ) e. ( SubMnd ` ( mulGrp ` S ) ) ) ) )
14 12 13 syl 
 |-  ( ( F e. ( S RingHom T ) /\ G e. ( S RingHom T ) ) -> ( dom ( F i^i G ) e. ( SubRing ` S ) <-> ( dom ( F i^i G ) e. ( SubGrp ` S ) /\ dom ( F i^i G ) e. ( SubMnd ` ( mulGrp ` S ) ) ) ) )
15 4 10 14 mpbir2and 
 |-  ( ( F e. ( S RingHom T ) /\ G e. ( S RingHom T ) ) -> dom ( F i^i G ) e. ( SubRing ` S ) )