Theorem rngohomcl

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

	Ref	Expression
Hypotheses	rnghomf.1	|- G = ( 1st ` R )
	rnghomf.2	|- X = ran G
	rnghomf.3	|- J = ( 1st ` S )
	rnghomf.4	|- Y = ran J
Assertion	rngohomcl	|- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ A e. X ) -> ( F ` A ) e. Y )

Proof

Step	Hyp	Ref	Expression
1		rnghomf.1	|- G = ( 1st ` R )
2		rnghomf.2	|- X = ran G
3		rnghomf.3	|- J = ( 1st ` S )
4		rnghomf.4	|- Y = ran J
5	1 2 3 4	rngohomf	|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F : X --> Y )
6	5	ffvelcdmda	|- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ A e. X ) -> ( F ` A ) e. Y )