Theorem rnghmf

Description: A ring homomorphism is a function. (Contributed by AV, 23-Feb-2020)

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

Proof

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