Metamath Proof Explorer


Theorem prmidlnr

Description: A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

Ref Expression
Hypotheses prmidlval.1 𝐵 = ( Base ‘ 𝑅 )
prmidlval.2 · = ( .r𝑅 )
Assertion prmidlnr ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑃𝐵 )

Proof

Step Hyp Ref Expression
1 prmidlval.1 𝐵 = ( Base ‘ 𝑅 )
2 prmidlval.2 · = ( .r𝑅 )
3 1 2 isprmidl ( 𝑅 ∈ Ring → ( 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃𝐵 ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎𝑃𝑏𝑃 ) ) ) ) )
4 3 biimpa ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃𝐵 ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥𝑎𝑦𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎𝑃𝑏𝑃 ) ) ) )
5 4 simp2d ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑃𝐵 )