pridlnr

Description: A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010)

	Ref	Expression
Hypotheses	pridlnr.1	$⊢ G = 1^{st} (R)$
	prdilnr.2	$⊢ X = ran G$
Assertion	pridlnr	$⊢ (R \in RingOps \land P \in PrIdl (R)) \to P \neq X$

Step	Hyp	Ref	Expression
1		pridlnr.1	$⊢ G = 1^{st} (R)$
2		prdilnr.2	$⊢ X = ran G$
3		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
4	1 3 2	ispridl	$⊢ R \in RingOps \to (P \in PrIdl (R) \leftrightarrow (P \in Idl (R) \land P \neq X \land \forall a \in Idl (R) \forall b \in Idl (R) (\forall x \in a \forall y \in b x 2^{nd} (R) y \in P \to (a \subseteq P \lor b \subseteq P))))$
5		3anan12	$⊢ (P \in Idl (R) \land P \neq X \land \forall a \in Idl (R) \forall b \in Idl (R) (\forall x \in a \forall y \in b x 2^{nd} (R) y \in P \to (a \subseteq P \lor b \subseteq P))) \leftrightarrow (P \neq X \land (P \in Idl (R) \land \forall a \in Idl (R) \forall b \in Idl (R) (\forall x \in a \forall y \in b x 2^{nd} (R) y \in P \to (a \subseteq P \lor b \subseteq P))))$
6	4 5	bitrdi	$⊢ R \in RingOps \to (P \in PrIdl (R) \leftrightarrow (P \neq X \land (P \in Idl (R) \land \forall a \in Idl (R) \forall b \in Idl (R) (\forall x \in a \forall y \in b x 2^{nd} (R) y \in P \to (a \subseteq P \lor b \subseteq P)))))$
7	6	simprbda	$⊢ (R \in RingOps \land P \in PrIdl (R)) \to P \neq X$

Metamath Proof Explorer