Theorem rhmf

Description: A ring homomorphism is a function. (Contributed by Stefan O'Rear, 8-Mar-2015)

	Ref	Expression
Hypotheses	rhmf.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rhmf.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
Assertion	rhmf	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : 𝐵 ⟶ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		rhmf.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rhmf.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
3		rhmghm	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
4	1 2	ghmf	⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐹 : 𝐵 ⟶ 𝐶 )
5	3 4	syl	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : 𝐵 ⟶ 𝐶 )