Metamath Proof Explorer

Theorem crngrhmfo

Description: The image of a surjective homomorphism from a commutative ring is commutative. (Contributed by Jeff Madsen, 4-Jan-2011) (Revised by AV, 19-Jul-2026)

Ref Expression
Hypothesis crngrhmfo.b 
|- B = ( Base ` S )
Assertion crngrhmfo 
|- ( ( R e. CRing /\ F e. ( R RingHom S ) /\ F : dom F -onto-> B ) -> S e. CRing )

Proof

Step Hyp Ref Expression
1 crngrhmfo.b 
 |-  B = ( Base ` S )
2 rhmrcl2 
 |-  ( F e. ( R RingHom S ) -> S e. Ring )
3 2 3ad2ant2 
 |-  ( ( R e. CRing /\ F e. ( R RingHom S ) /\ F : dom F -onto-> B ) -> S e. Ring )
4 foelrn 
 |-  ( ( F : dom F -onto-> B /\ x e. B ) -> E. a e. dom F x = ( F ` a ) )
5 4 ex 
 |-  ( F : dom F -onto-> B -> ( x e. B -> E. a e. dom F x = ( F ` a ) ) )
6 foelrn 
 |-  ( ( F : dom F -onto-> B /\ y e. B ) -> E. b e. dom F y = ( F ` b ) )
7 6 ex 
 |-  ( F : dom F -onto-> B -> ( y e. B -> E. b e. dom F y = ( F ` b ) ) )
8 5 7 anim12d 
 |-  ( F : dom F -onto-> B -> ( ( x e. B /\ y e. B ) -> ( E. a e. dom F x = ( F ` a ) /\ E. b e. dom F y = ( F ` b ) ) ) )
9 reeanv 
 |-  ( E. a e. dom F E. b e. dom F ( x = ( F ` a ) /\ y = ( F ` b ) ) <-> ( E. a e. dom F x = ( F ` a ) /\ E. b e. dom F y = ( F ` b ) ) )
10 8 9 imbitrrdi 
 |-  ( F : dom F -onto-> B -> ( ( x e. B /\ y e. B ) -> E. a e. dom F E. b e. dom F ( x = ( F ` a ) /\ y = ( F ` b ) ) ) )
11 10 3ad2ant3 
 |-  ( ( R e. CRing /\ F e. ( R RingHom S ) /\ F : dom F -onto-> B ) -> ( ( x e. B /\ y e. B ) -> E. a e. dom F E. b e. dom F ( x = ( F ` a ) /\ y = ( F ` b ) ) ) )
12 simpll 
 |-  ( ( ( R e. CRing /\ F e. ( R RingHom S ) ) /\ ( a e. dom F /\ b e. dom F ) ) -> R e. CRing )
13 eqid 
 |-  ( Base ` R ) = ( Base ` R )
14 eqid 
 |-  ( Base ` S ) = ( Base ` S )
15 13 14 rhmf 
 |-  ( F e. ( R RingHom S ) -> F : ( Base ` R ) --> ( Base ` S ) )
16 15 fdmd 
 |-  ( F e. ( R RingHom S ) -> dom F = ( Base ` R ) )
17 16 eleq2d 
 |-  ( F e. ( R RingHom S ) -> ( a e. dom F <-> a e. ( Base ` R ) ) )
18 16 eleq2d 
 |-  ( F e. ( R RingHom S ) -> ( b e. dom F <-> b e. ( Base ` R ) ) )
19 17 18 anbi12d 
 |-  ( F e. ( R RingHom S ) -> ( ( a e. dom F /\ b e. dom F ) <-> ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) )
20 19 biimpd 
 |-  ( F e. ( R RingHom S ) -> ( ( a e. dom F /\ b e. dom F ) -> ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) )
21 20 adantl 
 |-  ( ( R e. CRing /\ F e. ( R RingHom S ) ) -> ( ( a e. dom F /\ b e. dom F ) -> ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) )
22 21 imp 
 |-  ( ( ( R e. CRing /\ F e. ( R RingHom S ) ) /\ ( a e. dom F /\ b e. dom F ) ) -> ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) )
23 3anass 
 |-  ( ( R e. CRing /\ a e. ( Base ` R ) /\ b e. ( Base ` R ) ) <-> ( R e. CRing /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) )
24 12 22 23 sylanbrc 
 |-  ( ( ( R e. CRing /\ F e. ( R RingHom S ) ) /\ ( a e. dom F /\ b e. dom F ) ) -> ( R e. CRing /\ a e. ( Base ` R ) /\ b e. ( Base ` R ) ) )
25 eqid 
 |-  ( .r ` R ) = ( .r ` R )
26 13 25 crngcom 
 |-  ( ( R e. CRing /\ a e. ( Base ` R ) /\ b e. ( Base ` R ) ) -> ( a ( .r ` R ) b ) = ( b ( .r ` R ) a ) )
27 24 26 syl 
 |-  ( ( ( R e. CRing /\ F e. ( R RingHom S ) ) /\ ( a e. dom F /\ b e. dom F ) ) -> ( a ( .r ` R ) b ) = ( b ( .r ` R ) a ) )
28 27 fveq2d 
 |-  ( ( ( R e. CRing /\ F e. ( R RingHom S ) ) /\ ( a e. dom F /\ b e. dom F ) ) -> ( F ` ( a ( .r ` R ) b ) ) = ( F ` ( b ( .r ` R ) a ) ) )
29 simplr 
 |-  ( ( ( R e. CRing /\ F e. ( R RingHom S ) ) /\ ( a e. dom F /\ b e. dom F ) ) -> F e. ( R RingHom S ) )
30 3anass 
 |-  ( ( F e. ( R RingHom S ) /\ a e. ( Base ` R ) /\ b e. ( Base ` R ) ) <-> ( F e. ( R RingHom S ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) )
31 29 22 30 sylanbrc 
 |-  ( ( ( R e. CRing /\ F e. ( R RingHom S ) ) /\ ( a e. dom F /\ b e. dom F ) ) -> ( F e. ( R RingHom S ) /\ a e. ( Base ` R ) /\ b e. ( Base ` R ) ) )
32 eqid 
 |-  ( .r ` S ) = ( .r ` S )
33 13 25 32 rhmmul 
 |-  ( ( F e. ( R RingHom S ) /\ a e. ( Base ` R ) /\ b e. ( Base ` R ) ) -> ( F ` ( a ( .r ` R ) b ) ) = ( ( F ` a ) ( .r ` S ) ( F ` b ) ) )
34 31 33 syl 
 |-  ( ( ( R e. CRing /\ F e. ( R RingHom S ) ) /\ ( a e. dom F /\ b e. dom F ) ) -> ( F ` ( a ( .r ` R ) b ) ) = ( ( F ` a ) ( .r ` S ) ( F ` b ) ) )
35 22 ancomd 
 |-  ( ( ( R e. CRing /\ F e. ( R RingHom S ) ) /\ ( a e. dom F /\ b e. dom F ) ) -> ( b e. ( Base ` R ) /\ a e. ( Base ` R ) ) )
36 3anass 
 |-  ( ( F e. ( R RingHom S ) /\ b e. ( Base ` R ) /\ a e. ( Base ` R ) ) <-> ( F e. ( R RingHom S ) /\ ( b e. ( Base ` R ) /\ a e. ( Base ` R ) ) ) )
37 29 35 36 sylanbrc 
 |-  ( ( ( R e. CRing /\ F e. ( R RingHom S ) ) /\ ( a e. dom F /\ b e. dom F ) ) -> ( F e. ( R RingHom S ) /\ b e. ( Base ` R ) /\ a e. ( Base ` R ) ) )
38 13 25 32 rhmmul 
 |-  ( ( F e. ( R RingHom S ) /\ b e. ( Base ` R ) /\ a e. ( Base ` R ) ) -> ( F ` ( b ( .r ` R ) a ) ) = ( ( F ` b ) ( .r ` S ) ( F ` a ) ) )
39 37 38 syl 
 |-  ( ( ( R e. CRing /\ F e. ( R RingHom S ) ) /\ ( a e. dom F /\ b e. dom F ) ) -> ( F ` ( b ( .r ` R ) a ) ) = ( ( F ` b ) ( .r ` S ) ( F ` a ) ) )
40 28 34 39 3eqtr3d 
 |-  ( ( ( R e. CRing /\ F e. ( R RingHom S ) ) /\ ( a e. dom F /\ b e. dom F ) ) -> ( ( F ` a ) ( .r ` S ) ( F ` b ) ) = ( ( F ` b ) ( .r ` S ) ( F ` a ) ) )
41 oveq12 
 |-  ( ( x = ( F ` a ) /\ y = ( F ` b ) ) -> ( x ( .r ` S ) y ) = ( ( F ` a ) ( .r ` S ) ( F ` b ) ) )
42 oveq12 
 |-  ( ( y = ( F ` b ) /\ x = ( F ` a ) ) -> ( y ( .r ` S ) x ) = ( ( F ` b ) ( .r ` S ) ( F ` a ) ) )
43 42 ancoms 
 |-  ( ( x = ( F ` a ) /\ y = ( F ` b ) ) -> ( y ( .r ` S ) x ) = ( ( F ` b ) ( .r ` S ) ( F ` a ) ) )
44 41 43 eqeq12d 
 |-  ( ( x = ( F ` a ) /\ y = ( F ` b ) ) -> ( ( x ( .r ` S ) y ) = ( y ( .r ` S ) x ) <-> ( ( F ` a ) ( .r ` S ) ( F ` b ) ) = ( ( F ` b ) ( .r ` S ) ( F ` a ) ) ) )
45 40 44 syl5ibrcom 
 |-  ( ( ( R e. CRing /\ F e. ( R RingHom S ) ) /\ ( a e. dom F /\ b e. dom F ) ) -> ( ( x = ( F ` a ) /\ y = ( F ` b ) ) -> ( x ( .r ` S ) y ) = ( y ( .r ` S ) x ) ) )
46 45 ex 
 |-  ( ( R e. CRing /\ F e. ( R RingHom S ) ) -> ( ( a e. dom F /\ b e. dom F ) -> ( ( x = ( F ` a ) /\ y = ( F ` b ) ) -> ( x ( .r ` S ) y ) = ( y ( .r ` S ) x ) ) ) )
47 46 3adant3 
 |-  ( ( R e. CRing /\ F e. ( R RingHom S ) /\ F : dom F -onto-> B ) -> ( ( a e. dom F /\ b e. dom F ) -> ( ( x = ( F ` a ) /\ y = ( F ` b ) ) -> ( x ( .r ` S ) y ) = ( y ( .r ` S ) x ) ) ) )
48 47 rexlimdvv 
 |-  ( ( R e. CRing /\ F e. ( R RingHom S ) /\ F : dom F -onto-> B ) -> ( E. a e. dom F E. b e. dom F ( x = ( F ` a ) /\ y = ( F ` b ) ) -> ( x ( .r ` S ) y ) = ( y ( .r ` S ) x ) ) )
49 11 48 syld 
 |-  ( ( R e. CRing /\ F e. ( R RingHom S ) /\ F : dom F -onto-> B ) -> ( ( x e. B /\ y e. B ) -> ( x ( .r ` S ) y ) = ( y ( .r ` S ) x ) ) )
50 49 ralrimivv 
 |-  ( ( R e. CRing /\ F e. ( R RingHom S ) /\ F : dom F -onto-> B ) -> A. x e. B A. y e. B ( x ( .r ` S ) y ) = ( y ( .r ` S ) x ) )
51 1 32 iscrng2 
 |-  ( S e. CRing <-> ( S e. Ring /\ A. x e. B A. y e. B ( x ( .r ` S ) y ) = ( y ( .r ` S ) x ) ) )
52 3 50 51 sylanbrc 
 |-  ( ( R e. CRing /\ F e. ( R RingHom S ) /\ F : dom F -onto-> B ) -> S e. CRing )