Theorem rhmrcl1

Description: Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015)

	Ref	Expression
Assertion	rhmrcl1	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		dfrhm2	⊢ RingHom = ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) )
2	1	elmpocl1	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )