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 ‘ 𝑅 ) ) → 𝑃 ≠ 𝐵 )