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 crnghomfo.1 
|- G = ( 1st ` R )
crnghomfo.2 
|- X = ran G
crnghomfo.3 
|- J = ( 1st ` S )
crnghomfo.4 
|- Y = ran J
Assertion crngohomfo 
|- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : X -onto-> Y ) ) -> S e. CRingOps )

Proof

Step Hyp Ref Expression
1 crnghomfo.1 
 |-  G = ( 1st ` R )
2 crnghomfo.2 
 |-  X = ran G
3 crnghomfo.3 
 |-  J = ( 1st ` S )
4 crnghomfo.4 
 |-  Y = ran J
5 simplr 
 |-  ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : X -onto-> Y ) ) -> S e. RingOps )
6 foelrn 
 |-  ( ( F : X -onto-> Y /\ y e. Y ) -> E. w e. X y = ( F ` w ) )
7 6 ex 
 |-  ( F : X -onto-> Y -> ( y e. Y -> E. w e. X y = ( F ` w ) ) )
8 foelrn 
 |-  ( ( F : X -onto-> Y /\ z e. Y ) -> E. x e. X z = ( F ` x ) )
9 8 ex 
 |-  ( F : X -onto-> Y -> ( z e. Y -> E. x e. X z = ( F ` x ) ) )
10 7 9 anim12d 
 |-  ( F : X -onto-> Y -> ( ( y e. Y /\ z e. Y ) -> ( E. w e. X y = ( F ` w ) /\ E. x e. X z = ( F ` x ) ) ) )
11 reeanv 
 |-  ( E. w e. X E. x e. X ( y = ( F ` w ) /\ z = ( F ` x ) ) <-> ( E. w e. X y = ( F ` w ) /\ E. x e. X z = ( F ` x ) ) )
12 10 11 syl6ibr 
 |-  ( F : X -onto-> Y -> ( ( y e. Y /\ z e. Y ) -> E. w e. X E. x e. X ( y = ( F ` w ) /\ z = ( F ` x ) ) ) )
13 12 ad2antll 
 |-  ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom 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 ) ) ) )
14 eqid 
 |-  ( 2nd ` R ) = ( 2nd ` R )
15 1 14 2 crngocom 
 |-  ( ( R e. CRingOps /\ w e. X /\ x e. X ) -> ( w ( 2nd ` R ) x ) = ( x ( 2nd ` R ) w ) )
16 15 3expb 
 |-  ( ( R e. CRingOps /\ ( w e. X /\ x e. X ) ) -> ( w ( 2nd ` R ) x ) = ( x ( 2nd ` R ) w ) )
17 16 3ad2antl1 
 |-  ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( w ( 2nd ` R ) x ) = ( x ( 2nd ` R ) w ) )
18 17 fveq2d 
 |-  ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( w ( 2nd ` R ) x ) ) = ( F ` ( x ( 2nd ` R ) w ) ) )
19 crngorngo 
 |-  ( R e. CRingOps -> R e. RingOps )
20 eqid 
 |-  ( 2nd ` S ) = ( 2nd ` S )
21 1 2 14 20 rngohommul 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( w ( 2nd ` R ) x ) ) = ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) )
22 19 21 syl3anl1 
 |-  ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( w ( 2nd ` R ) x ) ) = ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) )
23 1 2 14 20 rngohommul 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( x e. X /\ w e. X ) ) -> ( F ` ( x ( 2nd ` R ) w ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) )
24 23 ancom2s 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( x ( 2nd ` R ) w ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) )
25 19 24 syl3anl1 
 |-  ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( x ( 2nd ` R ) w ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) )
26 18 22 25 3eqtr3d 
 |-  ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) )
27 oveq12 
 |-  ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) )
28 oveq12 
 |-  ( ( z = ( F ` x ) /\ y = ( F ` w ) ) -> ( z ( 2nd ` S ) y ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) )
29 28 ancoms 
 |-  ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( z ( 2nd ` S ) y ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) )
30 27 29 eqeq12d 
 |-  ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) <-> ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) )
31 26 30 syl5ibrcom 
 |-  ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) )
32 31 ex 
 |-  ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( ( w e. X /\ x e. X ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) )
33 32 3expa 
 |-  ( ( ( R e. CRingOps /\ S e. RingOps ) /\ F e. ( R RngHom S ) ) -> ( ( w e. X /\ x e. X ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) )
34 33 adantrr 
 |-  ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom 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 ) ) ) )
35 34 rexlimdvv 
 |-  ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom 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 ) ) )
36 13 35 syld 
 |-  ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : X -onto-> Y ) ) -> ( ( y e. Y /\ z e. Y ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) )
37 36 ralrimivv 
 |-  ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : X -onto-> Y ) ) -> A. y e. Y A. z e. Y ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) )
38 3 20 4 iscrngo2 
 |-  ( S e. CRingOps <-> ( S e. RingOps /\ A. y e. Y A. z e. Y ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) )
39 5 37 38 sylanbrc 
 |-  ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : X -onto-> Y ) ) -> S e. CRingOps )