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 ‘ 𝑆 ) )