Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prmidl Structured version   Visualization version   GIF version

Theorem prmidl 30967
 Description: The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.)
Hypotheses
Ref Expression
prmidlval.1 𝐵 = (Base‘𝑅)
prmidlval.2 · = (.r𝑅)
Assertion
Ref Expression
prmidl ((((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐽 ∈ (LIdeal‘𝑅))) ∧ ∀𝑥𝐼𝑦𝐽 (𝑥 · 𝑦) ∈ 𝑃) → (𝐼𝑃𝐽𝑃))
Distinct variable groups:   𝑥,𝑅,𝑦   𝑥,𝑃,𝑦   𝑥,𝐼   𝑥,𝐽,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦)   · (𝑥,𝑦)   𝐼(𝑦)

Proof of Theorem prmidl
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 raleq 3390 . . . . 5 (𝑏 = 𝐽 → (∀𝑦𝑏 (𝑥 · 𝑦) ∈ 𝑃 ↔ ∀𝑦𝐽 (𝑥 · 𝑦) ∈ 𝑃))
21ralbidv 3185 . . . 4 (𝑏 = 𝐽 → (∀𝑥𝐼𝑦𝑏 (𝑥 · 𝑦) ∈ 𝑃 ↔ ∀𝑥𝐼𝑦𝐽 (𝑥 · 𝑦) ∈ 𝑃))
3 sseq1 3968 . . . . 5 (𝑏 = 𝐽 → (𝑏𝑃𝐽𝑃))
43orbi2d 913 . . . 4 (𝑏 = 𝐽 → ((𝐼𝑃𝑏𝑃) ↔ (𝐼𝑃𝐽𝑃)))
52, 4imbi12d 348 . . 3 (𝑏 = 𝐽 → ((∀𝑥𝐼𝑦𝑏 (𝑥 · 𝑦) ∈ 𝑃 → (𝐼𝑃𝑏𝑃)) ↔ (∀𝑥𝐼𝑦𝐽 (𝑥 · 𝑦) ∈ 𝑃 → (𝐼𝑃𝐽𝑃))))
6 raleq 3390 . . . . . 6 (𝑎 = 𝐼 → (∀𝑥𝑎𝑦𝑏 (𝑥 · 𝑦) ∈ 𝑃 ↔ ∀𝑥𝐼𝑦𝑏 (𝑥 · 𝑦) ∈ 𝑃))
7 sseq1 3968 . . . . . . 7 (𝑎 = 𝐼 → (𝑎𝑃𝐼𝑃))
87orbi1d 914 . . . . . 6 (𝑎 = 𝐼 → ((𝑎𝑃𝑏𝑃) ↔ (𝐼𝑃𝑏𝑃)))
96, 8imbi12d 348 . . . . 5 (𝑎 = 𝐼 → ((∀𝑥𝑎𝑦𝑏 (𝑥 · 𝑦) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) ↔ (∀𝑥𝐼𝑦𝑏 (𝑥 · 𝑦) ∈ 𝑃 → (𝐼𝑃𝑏𝑃))))
109ralbidv 3185 . . . 4 (𝑎 = 𝐼 → (∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥𝑎𝑦𝑏 (𝑥 · 𝑦) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) ↔ ∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥𝐼𝑦𝑏 (𝑥 · 𝑦) ∈ 𝑃 → (𝐼𝑃𝑏𝑃))))
11 prmidlval.1 . . . . . . . 8 𝐵 = (Base‘𝑅)
12 prmidlval.2 . . . . . . . 8 · = (.r𝑅)
1311, 12isprmidl 30965 . . . . . . 7 (𝑅 ∈ Ring → (𝑃 ∈ (PrmIdeal‘𝑅) ↔ (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃𝐵 ∧ ∀𝑎 ∈ (LIdeal‘𝑅)∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥𝑎𝑦𝑏 (𝑥 · 𝑦) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))))
1413biimpa 480 . . . . . 6 ((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃𝐵 ∧ ∀𝑎 ∈ (LIdeal‘𝑅)∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥𝑎𝑦𝑏 (𝑥 · 𝑦) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
1514simp3d 1141 . . . . 5 ((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → ∀𝑎 ∈ (LIdeal‘𝑅)∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥𝑎𝑦𝑏 (𝑥 · 𝑦) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))
1615adantr 484 . . . 4 (((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐽 ∈ (LIdeal‘𝑅))) → ∀𝑎 ∈ (LIdeal‘𝑅)∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥𝑎𝑦𝑏 (𝑥 · 𝑦) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))
17 simprl 770 . . . 4 (((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐽 ∈ (LIdeal‘𝑅))) → 𝐼 ∈ (LIdeal‘𝑅))
1810, 16, 17rspcdva 3602 . . 3 (((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐽 ∈ (LIdeal‘𝑅))) → ∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥𝐼𝑦𝑏 (𝑥 · 𝑦) ∈ 𝑃 → (𝐼𝑃𝑏𝑃)))
19 simprr 772 . . 3 (((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐽 ∈ (LIdeal‘𝑅))) → 𝐽 ∈ (LIdeal‘𝑅))
205, 18, 19rspcdva 3602 . 2 (((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐽 ∈ (LIdeal‘𝑅))) → (∀𝑥𝐼𝑦𝐽 (𝑥 · 𝑦) ∈ 𝑃 → (𝐼𝑃𝐽𝑃)))
2120imp 410 1 ((((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐽 ∈ (LIdeal‘𝑅))) ∧ ∀𝑥𝐼𝑦𝐽 (𝑥 · 𝑦) ∈ 𝑃) → (𝐼𝑃𝐽𝑃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115   ≠ wne 3007  ∀wral 3126   ⊆ wss 3910  ‘cfv 6328  (class class class)co 7130  Basecbs 16462  .rcmulr 16545  Ringcrg 19276  LIdealclidl 19918  PrmIdealcprmidl 30962 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pr 5303 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-ral 3131  df-rex 3132  df-rab 3135  df-v 3473  df-sbc 3750  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-opab 5102  df-mpt 5120  df-id 5433  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-iota 6287  df-fun 6330  df-fv 6336  df-ov 7133  df-prmidl 30963 This theorem is referenced by:  idlmulssprm  30969  isprmidlc  30974
 Copyright terms: Public domain W3C validator