Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  crngohomfo Structured version   Visualization version   GIF version

Theorem crngohomfo 37178
Description: The image of a homomorphism from a commutative ring is commutative. (Contributed by Jeff Madsen, 4-Jan-2011.)
Hypotheses
Ref Expression
crngohomfo.1 𝐺 = (1st𝑅)
crngohomfo.2 𝑋 = ran 𝐺
crngohomfo.3 𝐽 = (1st𝑆)
crngohomfo.4 𝑌 = ran 𝐽
Assertion
Ref Expression
crngohomfo (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐹:𝑋onto𝑌)) → 𝑆 ∈ CRingOps)

Proof of Theorem crngohomfo
Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplr 766 . 2 (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐹:𝑋onto𝑌)) → 𝑆 ∈ RingOps)
2 foelrn 7109 . . . . . . . 8 ((𝐹:𝑋onto𝑌𝑦𝑌) → ∃𝑤𝑋 𝑦 = (𝐹𝑤))
32ex 412 . . . . . . 7 (𝐹:𝑋onto𝑌 → (𝑦𝑌 → ∃𝑤𝑋 𝑦 = (𝐹𝑤)))
4 foelrn 7109 . . . . . . . 8 ((𝐹:𝑋onto𝑌𝑧𝑌) → ∃𝑥𝑋 𝑧 = (𝐹𝑥))
54ex 412 . . . . . . 7 (𝐹:𝑋onto𝑌 → (𝑧𝑌 → ∃𝑥𝑋 𝑧 = (𝐹𝑥)))
63, 5anim12d 608 . . . . . 6 (𝐹:𝑋onto𝑌 → ((𝑦𝑌𝑧𝑌) → (∃𝑤𝑋 𝑦 = (𝐹𝑤) ∧ ∃𝑥𝑋 𝑧 = (𝐹𝑥))))
7 reeanv 3225 . . . . . 6 (∃𝑤𝑋𝑥𝑋 (𝑦 = (𝐹𝑤) ∧ 𝑧 = (𝐹𝑥)) ↔ (∃𝑤𝑋 𝑦 = (𝐹𝑤) ∧ ∃𝑥𝑋 𝑧 = (𝐹𝑥)))
86, 7imbitrrdi 251 . . . . 5 (𝐹:𝑋onto𝑌 → ((𝑦𝑌𝑧𝑌) → ∃𝑤𝑋𝑥𝑋 (𝑦 = (𝐹𝑤) ∧ 𝑧 = (𝐹𝑥))))
98ad2antll 726 . . . 4 (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐹:𝑋onto𝑌)) → ((𝑦𝑌𝑧𝑌) → ∃𝑤𝑋𝑥𝑋 (𝑦 = (𝐹𝑤) ∧ 𝑧 = (𝐹𝑥))))
10 crngohomfo.1 . . . . . . . . . . . . . 14 𝐺 = (1st𝑅)
11 eqid 2731 . . . . . . . . . . . . . 14 (2nd𝑅) = (2nd𝑅)
12 crngohomfo.2 . . . . . . . . . . . . . 14 𝑋 = ran 𝐺
1310, 11, 12crngocom 37173 . . . . . . . . . . . . 13 ((𝑅 ∈ CRingOps ∧ 𝑤𝑋𝑥𝑋) → (𝑤(2nd𝑅)𝑥) = (𝑥(2nd𝑅)𝑤))
14133expb 1119 . . . . . . . . . . . 12 ((𝑅 ∈ CRingOps ∧ (𝑤𝑋𝑥𝑋)) → (𝑤(2nd𝑅)𝑥) = (𝑥(2nd𝑅)𝑤))
15143ad2antl1 1184 . . . . . . . . . . 11 (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝑤𝑋𝑥𝑋)) → (𝑤(2nd𝑅)𝑥) = (𝑥(2nd𝑅)𝑤))
1615fveq2d 6896 . . . . . . . . . 10 (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝑤𝑋𝑥𝑋)) → (𝐹‘(𝑤(2nd𝑅)𝑥)) = (𝐹‘(𝑥(2nd𝑅)𝑤)))
17 crngorngo 37172 . . . . . . . . . . 11 (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
18 eqid 2731 . . . . . . . . . . . 12 (2nd𝑆) = (2nd𝑆)
1910, 12, 11, 18rngohommul 37142 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝑤𝑋𝑥𝑋)) → (𝐹‘(𝑤(2nd𝑅)𝑥)) = ((𝐹𝑤)(2nd𝑆)(𝐹𝑥)))
2017, 19syl3anl1 1411 . . . . . . . . . 10 (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝑤𝑋𝑥𝑋)) → (𝐹‘(𝑤(2nd𝑅)𝑥)) = ((𝐹𝑤)(2nd𝑆)(𝐹𝑥)))
2110, 12, 11, 18rngohommul 37142 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝑥𝑋𝑤𝑋)) → (𝐹‘(𝑥(2nd𝑅)𝑤)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑤)))
2221ancom2s 647 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝑤𝑋𝑥𝑋)) → (𝐹‘(𝑥(2nd𝑅)𝑤)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑤)))
2317, 22syl3anl1 1411 . . . . . . . . . 10 (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝑤𝑋𝑥𝑋)) → (𝐹‘(𝑥(2nd𝑅)𝑤)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑤)))
2416, 20, 233eqtr3d 2779 . . . . . . . . 9 (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝑤𝑋𝑥𝑋)) → ((𝐹𝑤)(2nd𝑆)(𝐹𝑥)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑤)))
25 oveq12 7421 . . . . . . . . . 10 ((𝑦 = (𝐹𝑤) ∧ 𝑧 = (𝐹𝑥)) → (𝑦(2nd𝑆)𝑧) = ((𝐹𝑤)(2nd𝑆)(𝐹𝑥)))
26 oveq12 7421 . . . . . . . . . . 11 ((𝑧 = (𝐹𝑥) ∧ 𝑦 = (𝐹𝑤)) → (𝑧(2nd𝑆)𝑦) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑤)))
2726ancoms 458 . . . . . . . . . 10 ((𝑦 = (𝐹𝑤) ∧ 𝑧 = (𝐹𝑥)) → (𝑧(2nd𝑆)𝑦) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑤)))
2825, 27eqeq12d 2747 . . . . . . . . 9 ((𝑦 = (𝐹𝑤) ∧ 𝑧 = (𝐹𝑥)) → ((𝑦(2nd𝑆)𝑧) = (𝑧(2nd𝑆)𝑦) ↔ ((𝐹𝑤)(2nd𝑆)(𝐹𝑥)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑤))))
2924, 28syl5ibrcom 246 . . . . . . . 8 (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝑤𝑋𝑥𝑋)) → ((𝑦 = (𝐹𝑤) ∧ 𝑧 = (𝐹𝑥)) → (𝑦(2nd𝑆)𝑧) = (𝑧(2nd𝑆)𝑦)))
3029ex 412 . . . . . . 7 ((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → ((𝑤𝑋𝑥𝑋) → ((𝑦 = (𝐹𝑤) ∧ 𝑧 = (𝐹𝑥)) → (𝑦(2nd𝑆)𝑧) = (𝑧(2nd𝑆)𝑦))))
31303expa 1117 . . . . . 6 (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → ((𝑤𝑋𝑥𝑋) → ((𝑦 = (𝐹𝑤) ∧ 𝑧 = (𝐹𝑥)) → (𝑦(2nd𝑆)𝑧) = (𝑧(2nd𝑆)𝑦))))
3231adantrr 714 . . . . 5 (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐹:𝑋onto𝑌)) → ((𝑤𝑋𝑥𝑋) → ((𝑦 = (𝐹𝑤) ∧ 𝑧 = (𝐹𝑥)) → (𝑦(2nd𝑆)𝑧) = (𝑧(2nd𝑆)𝑦))))
3332rexlimdvv 3209 . . . 4 (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐹:𝑋onto𝑌)) → (∃𝑤𝑋𝑥𝑋 (𝑦 = (𝐹𝑤) ∧ 𝑧 = (𝐹𝑥)) → (𝑦(2nd𝑆)𝑧) = (𝑧(2nd𝑆)𝑦)))
349, 33syld 47 . . 3 (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐹:𝑋onto𝑌)) → ((𝑦𝑌𝑧𝑌) → (𝑦(2nd𝑆)𝑧) = (𝑧(2nd𝑆)𝑦)))
3534ralrimivv 3197 . 2 (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐹:𝑋onto𝑌)) → ∀𝑦𝑌𝑧𝑌 (𝑦(2nd𝑆)𝑧) = (𝑧(2nd𝑆)𝑦))
36 crngohomfo.3 . . 3 𝐽 = (1st𝑆)
37 crngohomfo.4 . . 3 𝑌 = ran 𝐽
3836, 18, 37iscrngo2 37169 . 2 (𝑆 ∈ CRingOps ↔ (𝑆 ∈ RingOps ∧ ∀𝑦𝑌𝑧𝑌 (𝑦(2nd𝑆)𝑧) = (𝑧(2nd𝑆)𝑦)))
391, 35, 38sylanbrc 582 1 (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐹:𝑋onto𝑌)) → 𝑆 ∈ CRingOps)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086   = wceq 1540  wcel 2105  wral 3060  wrex 3069  ran crn 5678  ontowfo 6542  cfv 6544  (class class class)co 7412  1st c1st 7976  2nd c2nd 7977  RingOpscrngo 37066   RingOpsHom crngohom 37132  CRingOpsccring 37165
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fo 6550  df-fv 6552  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7978  df-2nd 7979  df-map 8825  df-rngo 37067  df-rngohom 37135  df-com2 37162  df-crngo 37166
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator