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 35308
Description: A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 35340 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 35286 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ 𝑟 ∈ (Idl‘𝑅)) → 𝑟𝑋)
4 ssralv 4031 . . . . . . . . . . . . 13 (𝑟𝑋 → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
53, 4syl 17 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑟 ∈ (Idl‘𝑅)) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
65adantrr 715 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝑟 ∈ (Idl‘𝑅) ∧ 𝑠 ∈ (Idl‘𝑅))) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
71, 2idlss 35286 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ 𝑠 ∈ (Idl‘𝑅)) → 𝑠𝑋)
8 ssralv 4031 . . . . . . . . . . . . . 14 (𝑠𝑋 → (∀𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
98ralimdv 3176 . . . . . . . . . . . . 13 (𝑠𝑋 → (∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
107, 9syl 17 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑠 ∈ (Idl‘𝑅)) → (∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
1110adantrl 714 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝑟 ∈ (Idl‘𝑅) ∧ 𝑠 ∈ (Idl‘𝑅))) → (∀𝑎𝑟𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
126, 11syld 47 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ (𝑟 ∈ (Idl‘𝑅) ∧ 𝑠 ∈ (Idl‘𝑅))) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
1312adantlr 713 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑟 ∈ (Idl‘𝑅) ∧ 𝑠 ∈ (Idl‘𝑅))) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
14 r19.26-2 3169 . . . . . . . . . . 11 (∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 ∧ ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) ↔ (∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 ∧ ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
15 pm3.35 801 . . . . . . . . . . . . 13 (((𝑎𝐻𝑏) ∈ 𝑃 ∧ ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → (𝑎𝑃𝑏𝑃))
16152ralimi 3159 . . . . . . . . . . . 12 (∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 ∧ ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → ∀𝑎𝑟𝑏𝑠 (𝑎𝑃𝑏𝑃))
17 2ralor 3368 . . . . . . . . . . . . 13 (∀𝑎𝑟𝑏𝑠 (𝑎𝑃𝑏𝑃) ↔ (∀𝑎𝑟 𝑎𝑃 ∨ ∀𝑏𝑠 𝑏𝑃))
18 dfss3 3954 . . . . . . . . . . . . . 14 (𝑟𝑃 ↔ ∀𝑎𝑟 𝑎𝑃)
19 dfss3 3954 . . . . . . . . . . . . . 14 (𝑠𝑃 ↔ ∀𝑏𝑠 𝑏𝑃)
2018, 19orbi12i 910 . . . . . . . . . . . . 13 ((𝑟𝑃𝑠𝑃) ↔ (∀𝑎𝑟 𝑎𝑃 ∨ ∀𝑏𝑠 𝑏𝑃))
2117, 20sylbb2 240 . . . . . . . . . . . 12 (∀𝑎𝑟𝑏𝑠 (𝑎𝑃𝑏𝑃) → (𝑟𝑃𝑠𝑃))
2216, 21syl 17 . . . . . . . . . . 11 (∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 ∧ ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → (𝑟𝑃𝑠𝑃))
2314, 22sylbir 237 . . . . . . . . . 10 ((∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 ∧ ∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → (𝑟𝑃𝑠𝑃))
2423expcom 416 . . . . . . . . 9 (∀𝑎𝑟𝑏𝑠 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → (∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))
2513, 24syl6 35 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑟 ∈ (Idl‘𝑅) ∧ 𝑠 ∈ (Idl‘𝑅))) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → (∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))))
2625ralrimdvva 3192 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (Idl‘𝑅)) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))))
2726ex 415 . . . . . 6 (𝑅 ∈ RingOps → (𝑃 ∈ (Idl‘𝑅) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
2827adantrd 494 . . . . 5 (𝑅 ∈ RingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) → (∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)) → ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
2928imdistand 573 . . . 4 (𝑅 ∈ RingOps → (((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
30 df-3an 1083 . . . 4 ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))))
31 df-3an 1083 . . . 4 ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃))))
3229, 30, 313imtr4g 298 . . 3 (𝑅 ∈ RingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
33 ispridl2.2 . . . 4 𝐻 = (2nd𝑅)
341, 33, 2ispridl 35304 . . 3 (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑎𝑟𝑏𝑠 (𝑎𝐻𝑏) ∈ 𝑃 → (𝑟𝑃𝑠𝑃)))))
3532, 34sylibrd 261 . 2 (𝑅 ∈ RingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃))) → 𝑃 ∈ (PrIdl‘𝑅)))
3635imp 409 1 ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃𝑋 ∧ ∀𝑎𝑋𝑏𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎𝑃𝑏𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wo 843  w3a 1081   = wceq 1530  wcel 2107  wne 3014  wral 3136  wss 3934  ran crn 5549  cfv 6348  (class class class)co 7148  1st c1st 7679  2nd c2nd 7680  RingOpscrngo 35164  Idlcidl 35277  PrIdlcpridl 35278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-iota 6307  df-fun 6350  df-fv 6356  df-ov 7151  df-idl 35280  df-pridl 35281
This theorem is referenced by:  ispridlc  35340
  Copyright terms: Public domain W3C validator