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 ⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion crngrhmfo ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : dom 𝐹 –onto→ 𝐵 ) → 𝑆 ∈ CRing )

Proof

Step Hyp Ref Expression
1 crngrhmfo.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
2 rhmrcl2 ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
3 2 3ad2ant2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : dom 𝐹 –onto→ 𝐵 ) → 𝑆 ∈ Ring )
4 foelrn ⊢ ( ( 𝐹 : dom 𝐹 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑎 ∈ dom 𝐹 𝑥 = ( 𝐹 ‘ 𝑎 ) )
5 4 ex ⊢ ( 𝐹 : dom 𝐹 –onto→ 𝐵 → ( 𝑥 ∈ 𝐵 → ∃ 𝑎 ∈ dom 𝐹 𝑥 = ( 𝐹 ‘ 𝑎 ) ) )
6 foelrn ⊢ ( ( 𝐹 : dom 𝐹 –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑏 ∈ dom 𝐹 𝑦 = ( 𝐹 ‘ 𝑏 ) )
7 6 ex ⊢ ( 𝐹 : dom 𝐹 –onto→ 𝐵 → ( 𝑦 ∈ 𝐵 → ∃ 𝑏 ∈ dom 𝐹 𝑦 = ( 𝐹 ‘ 𝑏 ) ) )
8 5 7 anim12d ⊢ ( 𝐹 : dom 𝐹 –onto→ 𝐵 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑎 ∈ dom 𝐹 𝑥 = ( 𝐹 ‘ 𝑎 ) ∧ ∃ 𝑏 ∈ dom 𝐹 𝑦 = ( 𝐹 ‘ 𝑏 ) ) ) )
9 reeanv ⊢ ( ∃ 𝑎 ∈ dom 𝐹 ∃ 𝑏 ∈ dom 𝐹 ( 𝑥 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑏 ) ) ↔ ( ∃ 𝑎 ∈ dom 𝐹 𝑥 = ( 𝐹 ‘ 𝑎 ) ∧ ∃ 𝑏 ∈ dom 𝐹 𝑦 = ( 𝐹 ‘ 𝑏 ) ) )
10 8 9 imbitrrdi ⊢ ( 𝐹 : dom 𝐹 –onto→ 𝐵 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑎 ∈ dom 𝐹 ∃ 𝑏 ∈ dom 𝐹 ( 𝑥 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑏 ) ) ) )
11 10 3ad2ant3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : dom 𝐹 –onto→ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑎 ∈ dom 𝐹 ∃ 𝑏 ∈ dom 𝐹 ( 𝑥 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑏 ) ) ) )
12 simpll ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) ) → 𝑅 ∈ CRing )
13 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
15 13 14 rhmf ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
16 15 fdmd ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → dom 𝐹 = ( Base ‘ 𝑅 ) )
17 16 eleq2d ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝑎 ∈ dom 𝐹 ↔ 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
18 16 eleq2d ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝑏 ∈ dom 𝐹 ↔ 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
19 17 18 anbi12d ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) ↔ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) )
20 19 biimpd ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) )
21 20 adantl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) → ( ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) )
22 21 imp ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
23 3anass ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ↔ ( 𝑅 ∈ CRing ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) )
24 12 22 23 sylanbrc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) ) → ( 𝑅 ∈ CRing ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
25 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
26 13 25 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) )
27 24 26 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) )
28 27 fveq2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) ) )
29 simplr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
30 3anass ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ↔ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) )
31 29 22 30 sylanbrc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) ) → ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
32 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
33 13 25 32 rhmmul ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) )
34 31 33 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) )
35 22 ancomd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) ) → ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
36 3anass ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ↔ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ) )
37 29 35 36 sylanbrc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) ) → ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
38 13 25 32 rhmmul ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) ) = ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑎 ) ) )
39 37 38 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) ) → ( 𝐹 ‘ ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) ) = ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑎 ) ) )
40 28 34 39 3eqtr3d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) ) → ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑎 ) ) )
41 oveq12 ⊢ ( ( 𝑥 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑏 ) ) → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) )
42 oveq12 ⊢ ( ( 𝑦 = ( 𝐹 ‘ 𝑏 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑎 ) ) → ( 𝑦 ( .r ‘ 𝑆 ) 𝑥 ) = ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑎 ) ) )
43 42 ancoms ⊢ ( ( 𝑥 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑏 ) ) → ( 𝑦 ( .r ‘ 𝑆 ) 𝑥 ) = ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑎 ) ) )
44 41 43 eqeq12d ⊢ ( ( 𝑥 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑏 ) ) → ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑆 ) 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑎 ) ) ) )
45 40 44 syl5ibrcom ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) ) → ( ( 𝑥 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑏 ) ) → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑆 ) 𝑥 ) ) )
46 45 ex ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) → ( ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) → ( ( 𝑥 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑏 ) ) → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑆 ) 𝑥 ) ) ) )
47 46 3adant3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : dom 𝐹 –onto→ 𝐵 ) → ( ( 𝑎 ∈ dom 𝐹 ∧ 𝑏 ∈ dom 𝐹 ) → ( ( 𝑥 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑏 ) ) → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑆 ) 𝑥 ) ) ) )
48 47 rexlimdvv ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : dom 𝐹 –onto→ 𝐵 ) → ( ∃ 𝑎 ∈ dom 𝐹 ∃ 𝑏 ∈ dom 𝐹 ( 𝑥 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑏 ) ) → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑆 ) 𝑥 ) ) )
49 11 48 syld ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : dom 𝐹 –onto→ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑆 ) 𝑥 ) ) )
50 49 ralrimivv ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : dom 𝐹 –onto→ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑆 ) 𝑥 ) )
51 1 32 iscrng2 ⊢ ( 𝑆 ∈ CRing ↔ ( 𝑆 ∈ Ring ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑆 ) 𝑥 ) ) )
52 3 50 51 sylanbrc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : dom 𝐹 –onto→ 𝐵 ) → 𝑆 ∈ CRing )