pridl

Description: The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010)

		Ref	Expression
	Hypothesis	pridl.1	$⊢ H = 2^{nd} (R)$
	Assertion	pridl	$⊢ ((R \in RingOps \land P \in PrIdl (R)) \land (A \in Idl (R) \land B \in Idl (R) \land \forall x \in A \forall y \in B x H y \in P)) \to (A \subseteq P \lor B \subseteq P)$

Proof

Step	Hyp	Ref	Expression
1		pridl.1	$⊢ H = 2^{nd} (R)$
2		eqid	$⊢ 1^{st} (R) = 1^{st} (R)$
3		eqid	$⊢ ran 1^{st} (R) = ran 1^{st} (R)$
4	2 1 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 H y \in P \to (a \subseteq P \lor b \subseteq P))))$
5		df-3an	$⊢ (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 H 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 H 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 H y \in P \to (a \subseteq P \lor b \subseteq P))))$
7	6	simplbda	$⊢ (R \in RingOps \land P \in PrIdl (R)) \to \forall a \in Idl (R) \forall b \in Idl (R) (\forall x \in a \forall y \in b x H y \in P \to (a \subseteq P \lor b \subseteq P))$
8		raleq	$⊢ a = A \to (\forall x \in a \forall y \in b x H y \in P \leftrightarrow \forall x \in A \forall y \in b x H y \in P)$
9		sseq1	$⊢ a = A \to (a \subseteq P \leftrightarrow A \subseteq P)$
10	9	orbi1d	$⊢ a = A \to ((a \subseteq P \lor b \subseteq P) \leftrightarrow (A \subseteq P \lor b \subseteq P))$
11	8 10	imbi12d	$⊢ a = A \to ((\forall x \in a \forall y \in b x H y \in P \to (a \subseteq P \lor b \subseteq P)) \leftrightarrow (\forall x \in A \forall y \in b x H y \in P \to (A \subseteq P \lor b \subseteq P)))$
12		raleq	$⊢ b = B \to (\forall y \in b x H y \in P \leftrightarrow \forall y \in B x H y \in P)$
13	12	ralbidv	$⊢ b = B \to (\forall x \in A \forall y \in b x H y \in P \leftrightarrow \forall x \in A \forall y \in B x H y \in P)$
14		sseq1	$⊢ b = B \to (b \subseteq P \leftrightarrow B \subseteq P)$
15	14	orbi2d	$⊢ b = B \to ((A \subseteq P \lor b \subseteq P) \leftrightarrow (A \subseteq P \lor B \subseteq P))$
16	13 15	imbi12d	$⊢ b = B \to ((\forall x \in A \forall y \in b x H y \in P \to (A \subseteq P \lor b \subseteq P)) \leftrightarrow (\forall x \in A \forall y \in B x H y \in P \to (A \subseteq P \lor B \subseteq P)))$
17	11 16	rspc2v	$⊢ (A \in Idl (R) \land B \in Idl (R)) \to (\forall a \in Idl (R) \forall b \in Idl (R) (\forall x \in a \forall y \in b x H y \in P \to (a \subseteq P \lor b \subseteq P)) \to (\forall x \in A \forall y \in B x H y \in P \to (A \subseteq P \lor B \subseteq P)))$
18	7 17	syl5com	$⊢ (R \in RingOps \land P \in PrIdl (R)) \to ((A \in Idl (R) \land B \in Idl (R)) \to (\forall x \in A \forall y \in B x H y \in P \to (A \subseteq P \lor B \subseteq P)))$
19	18	expd	$⊢ (R \in RingOps \land P \in PrIdl (R)) \to (A \in Idl (R) \to (B \in Idl (R) \to (\forall x \in A \forall y \in B x H y \in P \to (A \subseteq P \lor B \subseteq P))))$
20	19	3imp2	$⊢ ((R \in RingOps \land P \in PrIdl (R)) \land (A \in Idl (R) \land B \in Idl (R) \land \forall x \in A \forall y \in B x H y \in P)) \to (A \subseteq P \lor B \subseteq P)$

Metamath Proof Explorer

Theorem pridl

Proof