Theorem rngohomadd

Description: Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011)

	Ref	Expression
Hypotheses	rnghomadd.1	$$⊢G=1^{st}\left(R\right)$$
	rnghomadd.2	$$⊢X=\mathrm{ran}G$$
	rnghomadd.3	$$⊢J=1^{st}\left(S\right)$$
Assertion	rngohomadd	Could not format assertion : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A G B ) ) = ( ( F ` A ) J ( F ` B ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rnghomadd.1	$$⊢G=1^{st}\left(R\right)$$
2		rnghomadd.2	$$⊢X=\mathrm{ran}G$$
3		rnghomadd.3	$$⊢J=1^{st}\left(S\right)$$
4		eqid	$$⊢2^{nd}\left(R\right)=2^{nd}\left(R\right)$$
5		eqid	$$⊢\mathrm{GId}\left(2^{nd}\left(R\right)\right)=\mathrm{GId}\left(2^{nd}\left(R\right)\right)$$
6		eqid	$$⊢2^{nd}\left(S\right)=2^{nd}\left(S\right)$$
7		eqid	$$⊢\mathrm{ran}J=\mathrm{ran}J$$
8		eqid	$$⊢\mathrm{GId}\left(2^{nd}\left(S\right)\right)=\mathrm{GId}\left(2^{nd}\left(S\right)\right)$$
9	1 4 2 5 3 6 7 8	isrngohom	Could not format ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsHom S ) <-> ( F : X --> ran J /\ ( 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 --> ran J /\ ( 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 --> ran J /\ ( 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 --> ran J /\ ( 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	simp3d	Could not format ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom 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 ) ) -> 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 |-
12	11	3impa	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom 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 ) ) -> 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 |-
13		simpl	$$⊢\left(F\left(xGy\right)=F\left(x\right)JF\left(y\right)\wedge F\left(x{2}^{nd}\left(R\right)y\right)=F\left(x\right)2^{nd}\left(S\right)F\left(y\right)\right)\to F\left(xGy\right)=F\left(x\right)JF\left(y\right)$$
14	13	2ralimi	$$⊢\forall x\in X\forall y\in X\left(F\left(xGy\right)=F\left(x\right)JF\left(y\right)\wedge F\left(x{2}^{nd}\left(R\right)y\right)=F\left(x\right)2^{nd}\left(S\right)F\left(y\right)\right)\to \forall x\in X\forall y\in XF\left(xGy\right)=F\left(x\right)JF\left(y\right)$$
15	12 14	syl	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> A. x e. X A. y e. X ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> A. x e. X A. y e. X ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) ) with typecode |-
16		fvoveq1	$$⊢x=A\to F\left(xGy\right)=F\left(AGy\right)$$
17		fveq2	$$⊢x=A\to F\left(x\right)=F\left(A\right)$$
18	17	oveq1d	$$⊢x=A\to F\left(x\right)JF\left(y\right)=F\left(A\right)JF\left(y\right)$$
19	16 18	eqeq12d	$$⊢x=A\to \left(F\left(xGy\right)=F\left(x\right)JF\left(y\right)\leftrightarrow F\left(AGy\right)=F\left(A\right)JF\left(y\right)\right)$$
20		oveq2	$$⊢y=B\to AGy=AGB$$
21	20	fveq2d	$$⊢y=B\to F\left(AGy\right)=F\left(AGB\right)$$
22		fveq2	$$⊢y=B\to F\left(y\right)=F\left(B\right)$$
23	22	oveq2d	$$⊢y=B\to F\left(A\right)JF\left(y\right)=F\left(A\right)JF\left(B\right)$$
24	21 23	eqeq12d	$$⊢y=B\to \left(F\left(AGy\right)=F\left(A\right)JF\left(y\right)\leftrightarrow F\left(AGB\right)=F\left(A\right)JF\left(B\right)\right)$$
25	19 24	rspc2v	$$⊢\left(A\in X\wedge B\in X\right)\to \left(\forall x\in X\forall y\in XF\left(xGy\right)=F\left(x\right)JF\left(y\right)\to F\left(AGB\right)=F\left(A\right)JF\left(B\right)\right)$$
26	15 25	mpan9	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A G B ) ) = ( ( F ` A ) J ( F ` B ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A G B ) ) = ( ( F ` A ) J ( F ` B ) ) ) with typecode |-