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	Could not format assertion : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ A e. X ) -> ( F ` A ) e. Y ) with typecode |-

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	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F : X --> Y ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F : X --> Y ) with typecode |-
6	5	ffvelcdmda	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ A e. X ) -> ( F ` A ) e. Y ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ A e. X ) -> ( F ` A ) e. Y ) with typecode |-