Theorem rhmf

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

	Ref	Expression
Hypotheses	rhmf.b	$$⊢B={\mathrm{Base}}_R$$
	rhmf.c	$$⊢C={\mathrm{Base}}_S$$
Assertion	rhmf	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F:B⟶C$$

Proof

Step	Hyp	Ref	Expression
1		rhmf.b	$$⊢B={\mathrm{Base}}_R$$
2		rhmf.c	$$⊢C={\mathrm{Base}}_S$$
3		rhmghm	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\in \left(R\mathrm{GrpHom}S\right)$$
4	1 2	ghmf	$$⊢F\in \left(R\mathrm{GrpHom}S\right)\to F:B⟶C$$
5	3 4	syl	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F:B⟶C$$