Metamath Proof Explorer


Theorem prmidl2

Description: A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

Ref Expression
Hypotheses prmidlval.1 𝐵 = ( Base ‘ 𝑅 )
prmidlval.2 · = ( .r𝑅 )
Assertion prmidl2 ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑃𝐵 ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 prmidlval.1 𝐵 = ( Base ‘ 𝑅 )
2 prmidlval.2 · = ( .r𝑅 )
3 simpr ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 )
4 simplrr ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → 𝑏 ∈ ( LIdeal ‘ 𝑅 ) )
5 eqid ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
6 1 5 lidlss ( 𝑏 ∈ ( LIdeal ‘ 𝑅 ) → 𝑏𝐵 )
7 4 6 syl ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → 𝑏𝐵 )
8 simplrl ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → 𝑎 ∈ ( LIdeal ‘ 𝑅 ) )
9 1 5 lidlss ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) → 𝑎𝐵 )
10 8 9 syl ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → 𝑎𝐵 )
11 simpllr ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) )
12 ssralv ( 𝑎𝐵 → ( ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) → ∀ 𝑥𝑎𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) )
13 10 11 12 sylc ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ∀ 𝑥𝑎𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) )
14 ssralv ( 𝑏𝐵 → ( ∀ 𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) → ∀ 𝑦𝑏 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) )
15 14 ralimdv ( 𝑏𝐵 → ( ∀ 𝑥𝑎𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) → ∀ 𝑥𝑎𝑦𝑏 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) )
16 7 13 15 sylc ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ∀ 𝑥𝑎𝑦𝑏 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) )
17 r19.26-2 ( ∀ 𝑥𝑎𝑦𝑏 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 ∧ ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) ↔ ( ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ∧ ∀ 𝑥𝑎𝑦𝑏 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) )
18 pm3.35 ( ( ( 𝑥 · 𝑦 ) ∈ 𝑃 ∧ ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) → ( 𝑥𝑃𝑦𝑃 ) )
19 18 2ralimi ( ∀ 𝑥𝑎𝑦𝑏 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 ∧ ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) → ∀ 𝑥𝑎𝑦𝑏 ( 𝑥𝑃𝑦𝑃 ) )
20 17 19 sylbir ( ( ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ∧ ∀ 𝑥𝑎𝑦𝑏 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) → ∀ 𝑥𝑎𝑦𝑏 ( 𝑥𝑃𝑦𝑃 ) )
21 3 16 20 syl2anc ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ∀ 𝑥𝑎𝑦𝑏 ( 𝑥𝑃𝑦𝑃 ) )
22 2ralor ( ∀ 𝑥𝑎𝑦𝑏 ( 𝑥𝑃𝑦𝑃 ) ↔ ( ∀ 𝑥𝑎 𝑥𝑃 ∨ ∀ 𝑦𝑏 𝑦𝑃 ) )
23 dfss3 ( 𝑎𝑃 ↔ ∀ 𝑥𝑎 𝑥𝑃 )
24 dfss3 ( 𝑏𝑃 ↔ ∀ 𝑦𝑏 𝑦𝑃 )
25 23 24 orbi12i ( ( 𝑎𝑃𝑏𝑃 ) ↔ ( ∀ 𝑥𝑎 𝑥𝑃 ∨ ∀ 𝑦𝑏 𝑦𝑃 ) )
26 22 25 sylbb2 ( ∀ 𝑥𝑎𝑦𝑏 ( 𝑥𝑃𝑦𝑃 ) → ( 𝑎𝑃𝑏𝑃 ) )
27 21 26 syl ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ( 𝑎𝑃𝑏𝑃 ) )
28 27 ex ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) → ( ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎𝑃𝑏𝑃 ) ) )
29 28 ralrimivva ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) → ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎𝑃𝑏𝑃 ) ) )
30 1 2 isprmidl ( 𝑅 ∈ Ring → ( 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃𝐵 ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎𝑃𝑏𝑃 ) ) ) ) )
31 30 biimpar ( ( 𝑅 ∈ Ring ∧ ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃𝐵 ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎𝑃𝑏𝑃 ) ) ) ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) )
32 31 3anassrs ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃𝐵 ) ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎𝑃𝑏𝑃 ) ) ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) )
33 29 32 syldan ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) )
34 33 anasss ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑃𝐵 ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) )