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	$⊢ B = {Base}_{R}$
	prmidlval.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	prmidlnr	$⊢ (R \in Ring \land P \in PrmIdeal (R)) \to P \neq B$

Step	Hyp	Ref	Expression
1		prmidlval.1	$⊢ B = {Base}_{R}$
2		prmidlval.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3	1 2	isprmidl	$⊢ R \in Ring \to (P \in PrmIdeal (R) \leftrightarrow (P \in LIdeal (R) \land P \neq B \land \forall a \in LIdeal (R) \forall b \in LIdeal (R) (\forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P \to (a \subseteq P \lor b \subseteq P))))$
4	3	biimpa	$⊢ (R \in Ring \land P \in PrmIdeal (R)) \to (P \in LIdeal (R) \land P \neq B \land \forall a \in LIdeal (R) \forall b \in LIdeal (R) (\forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P \to (a \subseteq P \lor b \subseteq P)))$
5	4	simp2d	$⊢ (R \in Ring \land P \in PrmIdeal (R)) \to P \neq B$

Metamath Proof Explorer