pridlidl

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

		Ref	Expression
	Assertion	pridlidl	$⊢ (R \in RingOps \land P \in PrIdl (R)) \to P \in Idl (R)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ 1^{st} (R) = 1^{st} (R)$
2		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
3		eqid	$⊢ ran 1^{st} (R) = ran 1^{st} (R)$
4	1 2 3	ispridl	$⊢ R \in RingOps \to (P \in PrIdl (R) \leftrightarrow (P \in Idl (R) \land P \neq ran 1^{st} (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))))$
5		3anass	$⊢ (P \in Idl (R) \land P \neq ran 1^{st} (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))) \leftrightarrow (P \in Idl (R) \land (P \neq ran 1^{st} (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 \in Idl (R) \land (P \neq ran 1^{st} (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 \in Idl (R)$

Metamath Proof Explorer