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

Theorem ispridl2 34374
Description: A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 34406 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 34352 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ 𝑟 ∈ (Idl‘𝑅)) → 𝑟𝑋)
4 ssralv 3891 . . . . . . . . . . . . 13 (𝑟𝑋 → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
53, 4syl 17 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑟 ∈ (Idl‘𝑅)) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
65adantrr 708 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝑟 ∈ (Idl‘𝑅) ∧ 𝑠 ∈ (Idl‘𝑅))) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
71, 2idlss 34352 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ 𝑠 ∈ (Idl‘𝑅)) → 𝑠𝑋)
8 ssralv 3891 . . . . . . . . . . . . . 14 (𝑠𝑋 → (∀𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
98ralimdv 3172 . . . . . . . . . . . . 13 (𝑠𝑋 → (∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
107, 9syl 17 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑠 ∈ (Idl‘𝑅)) → (∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
1110adantrl 707 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝑟 ∈ (Idl‘𝑅) ∧ 𝑠 ∈ (Idl‘𝑅))) → (∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
126, 11syld 47 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ (𝑟 ∈ (Idl‘𝑅) ∧ 𝑠 ∈ (Idl‘𝑅))) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
1312adantlr 706 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑟 ∈ (Idl‘𝑅) ∧ 𝑠 ∈ (Idl‘𝑅))) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
14 r19.26-2 3275 . . . . . . . . . . 11 (∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 ∧ ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) ↔ (∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 ∧ ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
15 pm3.35 837 . . . . . . . . . . . . 13 (((𝑎𝐻𝑏) ∈ 𝑃 ∧ ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → (𝑎𝑃𝑏𝑃))
16152ralimi 3162 . . . . . . . . . . . 12 (∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 ∧ ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → ∀𝑎𝑟𝑏𝑠 (𝑎𝑃𝑏𝑃))
17 2ralor 3319 . . . . . . . . . . . . 13 (∀𝑎𝑟𝑏𝑠 (𝑎𝑃𝑏𝑃) ↔ (∀𝑎𝑟 𝑎𝑃 ∨ ∀𝑏𝑠 𝑏𝑃))
18 dfss3 3816 . . . . . . . . . . . . . 14 (𝑟𝑃 ↔ ∀𝑎𝑟 𝑎𝑃)
19 dfss3 3816 . . . . . . . . . . . . . 14 (𝑠𝑃 ↔ ∀𝑏𝑠 𝑏𝑃)
2018, 19orbi12i 943 . . . . . . . . . . . . 13 ((𝑟𝑃𝑠𝑃) ↔ (∀𝑎𝑟 𝑎𝑃 ∨ ∀𝑏𝑠 𝑏𝑃))
2117, 20sylbb2 230 . . . . . . . . . . . 12 (∀𝑎𝑟𝑏𝑠 (𝑎𝑃𝑏𝑃) → (𝑟𝑃𝑠𝑃))
2216, 21syl 17 . . . . . . . . . . 11 (∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 ∧ ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → (𝑟𝑃𝑠𝑃))
2314, 22sylbir 227 . . . . . . . . . 10 ((∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 ∧ ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → (𝑟𝑃𝑠𝑃))
2423expcom 404 . . . . . . . . 9 (∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → (∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))
2513, 24syl6 35 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑟 ∈ (Idl‘𝑅) ∧ 𝑠 ∈ (Idl‘𝑅))) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → (∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))))
2625ralrimdvva 3183 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (Idl‘𝑅)) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))))
2726ex 403 . . . . . 6 (𝑅 ∈ RingOps → (𝑃 ∈ (Idl‘𝑅) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
2827adantrd 487 . . . . 5 (𝑅 ∈ RingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
2928imdistand 566 . . . 4 (𝑅 ∈ RingOps → (((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
30 df-3an 1113 . . . 4 ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
31 df-3an 1113 . . . 4 ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))))
3229, 30, 313imtr4g 288 . . 3 (𝑅 ∈ RingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
33 ispridl2.2 . . . 4 𝐻 = (2nd𝑅)
341, 33, 2ispridl 34370 . . 3 (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
3532, 34sylibrd 251 . 2 (𝑅 ∈ RingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → 𝑃 ∈ (PrIdl‘𝑅)))
3635imp 397 1 ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  wo 878  w3a 1111   = wceq 1656  wcel 2164  wne 2999  wral 3117  wss 3798  ran crn 5347  cfv 6127  (class class class)co 6910  1st c1st 7431  2nd c2nd 7432  RingOpscrngo 34230  Idlcidl 34343  PrIdlcpridl 34344
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-br 4876  df-opab 4938  df-mpt 4955  df-id 5252  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-iota 6090  df-fun 6129  df-fv 6135  df-ov 6913  df-idl 34346  df-pridl 34347
This theorem is referenced by:  ispridlc  34406
  Copyright terms: Public domain W3C validator