Theorem rngohomcl

Description: Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011)

	Ref	Expression
Hypotheses	rnghomf.1	$$⊢G=1^{st}\left(R\right)$$
	rnghomf.2	$$⊢X=\mathrm{ran}G$$
	rnghomf.3	$$⊢J=1^{st}\left(S\right)$$
	rnghomf.4	$$⊢Y=\mathrm{ran}J$$
Assertion	rngohomcl	$$⊢\left(\left(R\in \mathrm{RingOps}\wedge S\in \mathrm{RingOps}\wedge F\in \left(R\mathrm{RingOpsHom}S\right)\right)\wedge A\in X\right)\to F\left(A\right)\in Y$$

Proof

Step	Hyp	Ref	Expression
1		rnghomf.1	$$⊢G=1^{st}\left(R\right)$$
2		rnghomf.2	$$⊢X=\mathrm{ran}G$$
3		rnghomf.3	$$⊢J=1^{st}\left(S\right)$$
4		rnghomf.4	$$⊢Y=\mathrm{ran}J$$
5	1 2 3 4	rngohomf	$$⊢\left(R\in \mathrm{RingOps}\wedge S\in \mathrm{RingOps}\wedge F\in \left(R\mathrm{RingOpsHom}S\right)\right)\to F:X⟶Y$$
6	5	ffvelcdmda	$$⊢\left(\left(R\in \mathrm{RingOps}\wedge S\in \mathrm{RingOps}\wedge F\in \left(R\mathrm{RingOpsHom}S\right)\right)\wedge A\in X\right)\to F\left(A\right)\in Y$$