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 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
crnghomfo.2 ⊢ 𝑋 = ran 𝐺
crnghomfo.3 ⊢ 𝐽 = ( 1st ‘ 𝑆 )
crnghomfo.4 ⊢ 𝑌 = ran 𝐽
Assertion crngohomfo ( ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ) → 𝑆 ∈ CRingOps )

Proof

Step Hyp Ref Expression
1 crnghomfo.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 crnghomfo.2 ⊢ 𝑋 = ran 𝐺
3 crnghomfo.3 ⊢ 𝐽 = ( 1st ‘ 𝑆 )
4 crnghomfo.4 ⊢ 𝑌 = ran 𝐽
5 simplr ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ) → 𝑆 ∈ RingOps )
6 foelrn ⊢ ( ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ∃ 𝑤 ∈ 𝑋 𝑦 = ( 𝐹 ‘ 𝑤 ) )
7 6 ex ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ( 𝑦 ∈ 𝑌 → ∃ 𝑤 ∈ 𝑋 𝑦 = ( 𝐹 ‘ 𝑤 ) ) )
8 foelrn ⊢ ( ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝑧 ∈ 𝑌 ) → ∃ 𝑥 ∈ 𝑋 𝑧 = ( 𝐹 ‘ 𝑥 ) )
9 8 ex ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ( 𝑧 ∈ 𝑌 → ∃ 𝑥 ∈ 𝑋 𝑧 = ( 𝐹 ‘ 𝑥 ) ) )
10 7 9 anim12d ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑌 ) → ( ∃ 𝑤 ∈ 𝑋 𝑦 = ( 𝐹 ‘ 𝑤 ) ∧ ∃ 𝑥 ∈ 𝑋 𝑧 = ( 𝐹 ‘ 𝑥 ) ) ) )
11 reeanv ⊢ ( ∃ 𝑤 ∈ 𝑋 ∃ 𝑥 ∈ 𝑋 ( 𝑦 = ( 𝐹 ‘ 𝑤 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) ↔ ( ∃ 𝑤 ∈ 𝑋 𝑦 = ( 𝐹 ‘ 𝑤 ) ∧ ∃ 𝑥 ∈ 𝑋 𝑧 = ( 𝐹 ‘ 𝑥 ) ) )
12 10 11 syl6ibr ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑌 ) → ∃ 𝑤 ∈ 𝑋 ∃ 𝑥 ∈ 𝑋 ( 𝑦 = ( 𝐹 ‘ 𝑤 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) ) )
13 12 ad2antll ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ) → ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑌 ) → ∃ 𝑤 ∈ 𝑋 ∃ 𝑥 ∈ 𝑋 ( 𝑦 = ( 𝐹 ‘ 𝑤 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) ) )
14 eqid ⊢ ( 2nd ‘ 𝑅 ) = ( 2nd ‘ 𝑅 )
15 1 14 2 crngocom ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑤 ( 2nd ‘ 𝑅 ) 𝑥 ) = ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑤 ) )
16 15 3expb ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑤 ( 2nd ‘ 𝑅 ) 𝑥 ) = ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑤 ) )
17 16 3ad2antl1 ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑤 ( 2nd ‘ 𝑅 ) 𝑥 ) = ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑤 ) )
18 17 fveq2d ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑤 ( 2nd ‘ 𝑅 ) 𝑥 ) ) = ( 𝐹 ‘ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑤 ) ) )
19 crngorngo ⊢ ( 𝑅 ∈ CRingOps → 𝑅 ∈ RingOps )
20 eqid ⊢ ( 2nd ‘ 𝑆 ) = ( 2nd ‘ 𝑆 )
21 1 2 14 20 rngohommul ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑤 ( 2nd ‘ 𝑅 ) 𝑥 ) ) = ( ( 𝐹 ‘ 𝑤 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) )
22 19 21 syl3anl1 ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑤 ( 2nd ‘ 𝑅 ) 𝑥 ) ) = ( ( 𝐹 ‘ 𝑤 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) )
23 1 2 14 20 rngohommul ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑤 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑤 ) ) )
24 23 ancom2s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑤 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑤 ) ) )
25 19 24 syl3anl1 ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑤 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑤 ) ) )
26 18 22 25 3eqtr3d ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑤 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑤 ) ) )
27 oveq12 ⊢ ( ( 𝑦 = ( 𝐹 ‘ 𝑤 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑦 ( 2nd ‘ 𝑆 ) 𝑧 ) = ( ( 𝐹 ‘ 𝑤 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) )
28 oveq12 ⊢ ( ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑤 ) ) → ( 𝑧 ( 2nd ‘ 𝑆 ) 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑤 ) ) )
29 28 ancoms ⊢ ( ( 𝑦 = ( 𝐹 ‘ 𝑤 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑧 ( 2nd ‘ 𝑆 ) 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑤 ) ) )
30 27 29 eqeq12d ⊢ ( ( 𝑦 = ( 𝐹 ‘ 𝑤 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝑦 ( 2nd ‘ 𝑆 ) 𝑧 ) = ( 𝑧 ( 2nd ‘ 𝑆 ) 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑤 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑤 ) ) ) )
31 26 30 syl5ibrcom ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝑦 = ( 𝐹 ‘ 𝑤 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑦 ( 2nd ‘ 𝑆 ) 𝑧 ) = ( 𝑧 ( 2nd ‘ 𝑆 ) 𝑦 ) ) )
32 31 ex ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( ( 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 = ( 𝐹 ‘ 𝑤 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑦 ( 2nd ‘ 𝑆 ) 𝑧 ) = ( 𝑧 ( 2nd ‘ 𝑆 ) 𝑦 ) ) ) )
33 32 3expa ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( ( 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 = ( 𝐹 ‘ 𝑤 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑦 ( 2nd ‘ 𝑆 ) 𝑧 ) = ( 𝑧 ( 2nd ‘ 𝑆 ) 𝑦 ) ) ) )
34 33 adantrr ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ) → ( ( 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 = ( 𝐹 ‘ 𝑤 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑦 ( 2nd ‘ 𝑆 ) 𝑧 ) = ( 𝑧 ( 2nd ‘ 𝑆 ) 𝑦 ) ) ) )
35 34 rexlimdvv ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ) → ( ∃ 𝑤 ∈ 𝑋 ∃ 𝑥 ∈ 𝑋 ( 𝑦 = ( 𝐹 ‘ 𝑤 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑦 ( 2nd ‘ 𝑆 ) 𝑧 ) = ( 𝑧 ( 2nd ‘ 𝑆 ) 𝑦 ) ) )
36 13 35 syld ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ) → ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑌 ) → ( 𝑦 ( 2nd ‘ 𝑆 ) 𝑧 ) = ( 𝑧 ( 2nd ‘ 𝑆 ) 𝑦 ) ) )
37 36 ralrimivv ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ) → ∀ 𝑦 ∈ 𝑌 ∀ 𝑧 ∈ 𝑌 ( 𝑦 ( 2nd ‘ 𝑆 ) 𝑧 ) = ( 𝑧 ( 2nd ‘ 𝑆 ) 𝑦 ) )
38 3 20 4 iscrngo2 ⊢ ( 𝑆 ∈ CRingOps ↔ ( 𝑆 ∈ RingOps ∧ ∀ 𝑦 ∈ 𝑌 ∀ 𝑧 ∈ 𝑌 ( 𝑦 ( 2nd ‘ 𝑆 ) 𝑧 ) = ( 𝑧 ( 2nd ‘ 𝑆 ) 𝑦 ) ) )
39 5 37 38 sylanbrc ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ) → 𝑆 ∈ CRingOps )