Metamath Proof Explorer


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 R
crngohomfo.2 X = ran G
crngohomfo.3 J = 1 st S
crngohomfo.4 Y = 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 R
2 crngohomfo.2 X = ran G
3 crngohomfo.3 J = 1 st S
4 crngohomfo.4 Y = 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 F : X onto Y y Y w X y = F w
7 6 ex F : X onto Y y Y w X y = F w
8 foelrn F : X onto Y z Y x X z = F x
9 8 ex F : X onto Y z Y x X z = F x
10 7 9 anim12d F : X onto Y y Y z Y w X y = F w x X z = F x
11 reeanv w X x X y = F w z = F x w X y = F w x X z = F x
12 10 11 imbitrrdi F : X onto Y y Y z Y w X x X y = F w z = F x
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 R = 2 nd R
15 1 14 2 crngocom R CRingOps w X x X w 2 nd R x = x 2 nd R w
16 15 3expb R CRingOps w X x X w 2 nd R x = x 2 nd R 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 CRingOps R RingOps
20 eqid 2 nd S = 2 nd S
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 y = F w z = F x y 2 nd S z = F w 2 nd S F x
28 oveq12 z = F x y = F w z 2 nd S y = F x 2 nd S F w
29 28 ancoms y = F w z = F x z 2 nd S y = F x 2 nd S F w
30 27 29 eqeq12d y = F w z = F x y 2 nd S z = z 2 nd S y F w 2 nd S F x = F x 2 nd S F w
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 CRingOps S RingOps y Y z Y y 2 nd S z = z 2 nd S y
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 |-