Theorem crngohomfo

Description: The image of a homomorphism from a commutative ring is commutative. (Contributed by Jeff Madsen, 4-Jan-2011)

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

Proof

Step	Hyp	Ref	Expression
1		crngohomfo.1	$$⊢G=1^{st}\left(R\right)$$
2		crngohomfo.2	$$⊢X=\mathrm{ran}G$$
3		crngohomfo.3	$$⊢J=1^{st}\left(S\right)$$
4		crngohomfo.4	$$⊢Y=\mathrm{ran}J$$
5		simplr	Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> S e. RingOps ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> S e. RingOps ) with typecode |-
6		foelrn	$$⊢\left(F:X\underset{onto}{⟶}Y\wedge y\in Y\right)\to \exists w\in Xy=F\left(w\right)$$
7	6	ex	$$⊢F:X\underset{onto}{⟶}Y\to \left(y\in Y\to \exists w\in Xy=F\left(w\right)\right)$$
8		foelrn	$$⊢\left(F:X\underset{onto}{⟶}Y\wedge z\in Y\right)\to \exists x\in Xz=F\left(x\right)$$
9	8	ex	$$⊢F:X\underset{onto}{⟶}Y\to \left(z\in Y\to \exists x\in Xz=F\left(x\right)\right)$$
10	7 9	anim12d	$$⊢F:X\underset{onto}{⟶}Y\to \left(\left(y\in Y\wedge z\in Y\right)\to \left(\exists w\in Xy=F\left(w\right)\wedge \exists x\in Xz=F\left(x\right)\right)\right)$$
11		reeanv	$$⊢\exists w\in X\exists x\in X\left(y=F\left(w\right)\wedge z=F\left(x\right)\right)\leftrightarrow \left(\exists w\in Xy=F\left(w\right)\wedge \exists x\in Xz=F\left(x\right)\right)$$
12	10 11	imbitrrdi	$$⊢F:X\underset{onto}{⟶}Y\to \left(\left(y\in Y\wedge z\in Y\right)\to \exists w\in X\exists x\in X\left(y=F\left(w\right)\wedge z=F\left(x\right)\right)\right)$$
13	12	ad2antll	Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( ( y e. Y /\ z e. Y ) -> E. w e. X E. x e. X ( y = ( F ` w ) /\ z = ( F ` x ) ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( ( y e. Y /\ z e. Y ) -> E. w e. X E. x e. X ( y = ( F ` w ) /\ z = ( F ` x ) ) ) ) with typecode |-
14		eqid	$$⊢2^{nd}\left(R\right)=2^{nd}\left(R\right)$$
15	1 14 2	crngocom	$$⊢\left(R\in \mathrm{CRingOps}\wedge w\in X\wedge x\in X\right)\to w{2}^{nd}\left(R\right)x=x{2}^{nd}\left(R\right)w$$
16	15	3expb	$$⊢\left(R\in \mathrm{CRingOps}\wedge \left(w\in X\wedge x\in X\right)\right)\to w{2}^{nd}\left(R\right)x=x{2}^{nd}\left(R\right)w$$
17	16	3ad2antl1	Could not format ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( w ( 2nd ` R ) x ) = ( x ( 2nd ` R ) w ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( w ( 2nd ` R ) x ) = ( x ( 2nd ` R ) w ) ) with typecode |-
18	17	fveq2d	Could not format ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( w ( 2nd ` R ) x ) ) = ( F ` ( x ( 2nd ` R ) w ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( w ( 2nd ` R ) x ) ) = ( F ` ( x ( 2nd ` R ) w ) ) ) with typecode |-
19		crngorngo	$$⊢R\in \mathrm{CRingOps}\to R\in \mathrm{RingOps}$$
20		eqid	$$⊢2^{nd}\left(S\right)=2^{nd}\left(S\right)$$
21	1 2 14 20	rngohommul	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( w ( 2nd ` R ) x ) ) = ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( w ( 2nd ` R ) x ) ) = ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) ) with typecode |-
22	19 21	syl3anl1	Could not format ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( w ( 2nd ` R ) x ) ) = ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( w ( 2nd ` R ) x ) ) = ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) ) with typecode |-
23	1 2 14 20	rngohommul	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. X /\ w e. X ) ) -> ( F ` ( x ( 2nd ` R ) w ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. X /\ w e. X ) ) -> ( F ` ( x ( 2nd ` R ) w ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) with typecode |-
24	23	ancom2s	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( x ( 2nd ` R ) w ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( x ( 2nd ` R ) w ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) with typecode |-
25	19 24	syl3anl1	Could not format ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( x ( 2nd ` R ) w ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( x ( 2nd ` R ) w ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) with typecode |-
26	18 22 25	3eqtr3d	Could not format ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) with typecode |-
27		oveq12	$$⊢\left(y=F\left(w\right)\wedge z=F\left(x\right)\right)\to y{2}^{nd}\left(S\right)z=F\left(w\right)2^{nd}\left(S\right)F\left(x\right)$$
28		oveq12	$$⊢\left(z=F\left(x\right)\wedge y=F\left(w\right)\right)\to z{2}^{nd}\left(S\right)y=F\left(x\right)2^{nd}\left(S\right)F\left(w\right)$$
29	28	ancoms	$$⊢\left(y=F\left(w\right)\wedge z=F\left(x\right)\right)\to z{2}^{nd}\left(S\right)y=F\left(x\right)2^{nd}\left(S\right)F\left(w\right)$$
30	27 29	eqeq12d	$$⊢\left(y=F\left(w\right)\wedge z=F\left(x\right)\right)\to \left(y{2}^{nd}\left(S\right)z=z{2}^{nd}\left(S\right)y\leftrightarrow F\left(w\right)2^{nd}\left(S\right)F\left(x\right)=F\left(x\right)2^{nd}\left(S\right)F\left(w\right)\right)$$
31	26 30	syl5ibrcom	Could not format ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) with typecode |-
32	31	ex	Could not format ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( ( w e. X /\ x e. X ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) ) : No typesetting found for |- ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( ( w e. X /\ x e. X ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) ) with typecode |-
33	32	3expa	Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( w e. X /\ x e. X ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( w e. X /\ x e. X ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) ) with typecode |-
34	33	adantrr	Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( ( w e. X /\ x e. X ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( ( w e. X /\ x e. X ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) ) with typecode |-
35	34	rexlimdvv	Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( E. w e. X E. x e. X ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( E. w e. X E. x e. X ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) with typecode |-
36	13 35	syld	Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( ( y e. Y /\ z e. Y ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( ( y e. Y /\ z e. Y ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) with typecode |-
37	36	ralrimivv	Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> A. y e. Y A. z e. Y ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> A. y e. Y A. z e. Y ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) with typecode |-
38	3 20 4	iscrngo2	$$⊢S\in \mathrm{CRingOps}\leftrightarrow \left(S\in \mathrm{RingOps}\wedge \forall y\in Y\forall z\in Yy{2}^{nd}\left(S\right)z=z{2}^{nd}\left(S\right)y\right)$$
39	5 37 38	sylanbrc	Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> S e. CRingOps ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> S e. CRingOps ) with typecode |-