Theorem rngohomf

Description: A ring homomorphism is a function. (Contributed by Jeff Madsen, 19-Jun-2010)

	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	rngohomf	Could not format assertion : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F : X --> 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		eqid	$$⊢2^{nd}\left(R\right)=2^{nd}\left(R\right)$$
6		eqid	$$⊢\mathrm{GId}\left(2^{nd}\left(R\right)\right)=\mathrm{GId}\left(2^{nd}\left(R\right)\right)$$
7		eqid	$$⊢2^{nd}\left(S\right)=2^{nd}\left(S\right)$$
8		eqid	$$⊢\mathrm{GId}\left(2^{nd}\left(S\right)\right)=\mathrm{GId}\left(2^{nd}\left(S\right)\right)$$
9	1 5 2 6 3 7 4 8	isrngohom	Could not format ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsHom S ) <-> ( F : X --> Y /\ ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsHom S ) <-> ( F : X --> Y /\ ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) ) ) with typecode |-
10	9	biimpa	Could not format ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( F : X --> Y /\ ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( F : X --> Y /\ ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) ) with typecode |-
11	10	simp1d	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 |-
12	11	3impa	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 |-