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

Theorem ispridl2 35757
 Description: A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 35789 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.)
Hypotheses
Ref Expression
ispridl2.1 𝐺 = (1st𝑅)
ispridl2.2 𝐻 = (2nd𝑅)
ispridl2.3 𝑋 = ran 𝐺
Assertion
Ref Expression
ispridl2 ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅))
Distinct variable groups:   𝑅,𝑎,𝑏   𝑃,𝑎,𝑏   𝑋,𝑎,𝑏
Allowed substitution hints:   𝐺(𝑎,𝑏)   𝐻(𝑎,𝑏)

Proof of Theorem ispridl2
Dummy variables 𝑟 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ispridl2.1 . . . . . . . . . . . . . 14 𝐺 = (1st𝑅)
2 ispridl2.3 . . . . . . . . . . . . . 14 𝑋 = ran 𝐺
31, 2idlss 35735 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ 𝑟 ∈ (Idl‘𝑅)) → 𝑟𝑋)
4 ssralv 3959 . . . . . . . . . . . . 13 (𝑟𝑋 → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
53, 4syl 17 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑟 ∈ (Idl‘𝑅)) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
65adantrr 717 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝑟 ∈ (Idl‘𝑅) ∧ 𝑠 ∈ (Idl‘𝑅))) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
71, 2idlss 35735 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ 𝑠 ∈ (Idl‘𝑅)) → 𝑠𝑋)
8 ssralv 3959 . . . . . . . . . . . . . 14 (𝑠𝑋 → (∀𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
98ralimdv 3110 . . . . . . . . . . . . 13 (𝑠𝑋 → (∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
107, 9syl 17 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑠 ∈ (Idl‘𝑅)) → (∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
1110adantrl 716 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝑟 ∈ (Idl‘𝑅) ∧ 𝑠 ∈ (Idl‘𝑅))) → (∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
126, 11syld 47 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ (𝑟 ∈ (Idl‘𝑅) ∧ 𝑠 ∈ (Idl‘𝑅))) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
1312adantlr 715 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑟 ∈ (Idl‘𝑅) ∧ 𝑠 ∈ (Idl‘𝑅))) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
14 r19.26-2 3103 . . . . . . . . . . 11 (∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 ∧ ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) ↔ (∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 ∧ ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
15 pm3.35 803 . . . . . . . . . . . . 13 (((𝑎𝐻𝑏) ∈ 𝑃 ∧ ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → (𝑎𝑃𝑏𝑃))
16152ralimi 3094 . . . . . . . . . . . 12 (∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 ∧ ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → ∀𝑎𝑟𝑏𝑠 (𝑎𝑃𝑏𝑃))
17 2ralor 3288 . . . . . . . . . . . . 13 (∀𝑎𝑟𝑏𝑠 (𝑎𝑃𝑏𝑃) ↔ (∀𝑎𝑟 𝑎𝑃 ∨ ∀𝑏𝑠 𝑏𝑃))
18 dfss3 3881 . . . . . . . . . . . . . 14 (𝑟𝑃 ↔ ∀𝑎𝑟 𝑎𝑃)
19 dfss3 3881 . . . . . . . . . . . . . 14 (𝑠𝑃 ↔ ∀𝑏𝑠 𝑏𝑃)
2018, 19orbi12i 913 . . . . . . . . . . . . 13 ((𝑟𝑃𝑠𝑃) ↔ (∀𝑎𝑟 𝑎𝑃 ∨ ∀𝑏𝑠 𝑏𝑃))
2117, 20sylbb2 241 . . . . . . . . . . . 12 (∀𝑎𝑟𝑏𝑠 (𝑎𝑃𝑏𝑃) → (𝑟𝑃𝑠𝑃))
2216, 21syl 17 . . . . . . . . . . 11 (∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 ∧ ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → (𝑟𝑃𝑠𝑃))
2314, 22sylbir 238 . . . . . . . . . 10 ((∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 ∧ ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → (𝑟𝑃𝑠𝑃))
2423expcom 418 . . . . . . . . 9 (∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → (∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))
2513, 24syl6 35 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑟 ∈ (Idl‘𝑅) ∧ 𝑠 ∈ (Idl‘𝑅))) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → (∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))))
2625ralrimdvva 3124 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (Idl‘𝑅)) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))))
2726ex 417 . . . . . 6 (𝑅 ∈ RingOps → (𝑃 ∈ (Idl‘𝑅) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
2827adantrd 496 . . . . 5 (𝑅 ∈ RingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
2928imdistand 575 . . . 4 (𝑅 ∈ RingOps → (((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
30 df-3an 1087 . . . 4 ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
31 df-3an 1087 . . . 4 ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))))
3229, 30, 313imtr4g 300 . . 3 (𝑅 ∈ RingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
33 ispridl2.2 . . . 4 𝐻 = (2nd𝑅)
341, 33, 2ispridl 35753 . . 3 (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
3532, 34sylibrd 262 . 2 (𝑅 ∈ RingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → 𝑃 ∈ (PrIdl‘𝑅)))
3635imp 411 1 ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 845   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112   ≠ wne 2952  ∀wral 3071   ⊆ wss 3859  ran crn 5526  ‘cfv 6336  (class class class)co 7151  1st c1st 7692  2nd c2nd 7693  RingOpscrngo 35613  Idlcidl 35726  PrIdlcpridl 35727 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3698  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-iota 6295  df-fun 6338  df-fv 6344  df-ov 7154  df-idl 35729  df-pridl 35730 This theorem is referenced by:  ispridlc  35789
 Copyright terms: Public domain W3C validator