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 \in (S RingHom T) \land G \in (S RingHom T)) \to dom (F \cap G) \in SubRing (S)$

Proof

Step	Hyp	Ref	Expression
1		rhmghm	$⊢ F \in (S RingHom T) \to F \in (S GrpHom T)$
2		rhmghm	$⊢ G \in (S RingHom T) \to G \in (S GrpHom T)$
3		ghmeql	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to dom (F \cap G) \in SubGrp (S)$
4	1 2 3	syl2an	$⊢ (F \in (S RingHom T) \land G \in (S RingHom T)) \to dom (F \cap G) \in SubGrp (S)$
5		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
6		eqid	$⊢ {mulGrp}_{T} = {mulGrp}_{T}$
7	5 6	rhmmhm	$⊢ F \in (S RingHom T) \to F \in ({mulGrp}_{S} MndHom {mulGrp}_{T})$
8	5 6	rhmmhm	$⊢ G \in (S RingHom T) \to G \in ({mulGrp}_{S} MndHom {mulGrp}_{T})$
9		mhmeql	$⊢ (F \in ({mulGrp}_{S} MndHom {mulGrp}_{T}) \land G \in ({mulGrp}_{S} MndHom {mulGrp}_{T})) \to dom (F \cap G) \in SubMnd ({mulGrp}_{S})$
10	7 8 9	syl2an	$⊢ (F \in (S RingHom T) \land G \in (S RingHom T)) \to dom (F \cap G) \in SubMnd ({mulGrp}_{S})$
11		rhmrcl1	$⊢ F \in (S RingHom T) \to S \in Ring$
12	11	adantr	$⊢ (F \in (S RingHom T) \land G \in (S RingHom T)) \to S \in Ring$
13	5	issubrg3	$⊢ S \in Ring \to (dom (F \cap G) \in SubRing (S) \leftrightarrow (dom (F \cap G) \in SubGrp (S) \land dom (F \cap G) \in SubMnd ({mulGrp}_{S})))$
14	12 13	syl	$⊢ (F \in (S RingHom T) \land G \in (S RingHom T)) \to (dom (F \cap G) \in SubRing (S) \leftrightarrow (dom (F \cap G) \in SubGrp (S) \land dom (F \cap G) \in SubMnd ({mulGrp}_{S})))$
15	4 10 14	mpbir2and	$⊢ (F \in (S RingHom T) \land G \in (S RingHom T)) \to dom (F \cap G) \in SubRing (S)$