Theorem rnghmf

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

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

Proof

Step	Hyp	Ref	Expression
1		rnghmf.b	$$⊢B={\mathrm{Base}}_R$$
2		rnghmf.c	$$⊢C={\mathrm{Base}}_S$$
3		rnghmghm	$$⊢F\in \left(R\mathrm{RngHomo}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{RngHomo}S\right)\to F:B⟶C$$