prmidl

Description: The main property of a prime 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	prmidl	$⊢ (((R \in Ring \land P \in PrmIdeal (R)) \land (I \in LIdeal (R) \land J \in LIdeal (R))) \land \forall x \in I \forall y \in J x \underset{˙}{\cdot} y \in P) \to (I \subseteq P \lor J \subseteq P)$

Proof

Step	Hyp	Ref	Expression
1		prmidlval.1	$⊢ B = {Base}_{R}$
2		prmidlval.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		raleq	$⊢ b = J \to (\forall y \in b x \underset{˙}{\cdot} y \in P \leftrightarrow \forall y \in J x \underset{˙}{\cdot} y \in P)$
4	3	ralbidv	$⊢ b = J \to (\forall x \in I \forall y \in b x \underset{˙}{\cdot} y \in P \leftrightarrow \forall x \in I \forall y \in J x \underset{˙}{\cdot} y \in P)$
5		sseq1	$⊢ b = J \to (b \subseteq P \leftrightarrow J \subseteq P)$
6	5	orbi2d	$⊢ b = J \to ((I \subseteq P \lor b \subseteq P) \leftrightarrow (I \subseteq P \lor J \subseteq P))$
7	4 6	imbi12d	$⊢ b = J \to ((\forall x \in I \forall y \in b x \underset{˙}{\cdot} y \in P \to (I \subseteq P \lor b \subseteq P)) \leftrightarrow (\forall x \in I \forall y \in J x \underset{˙}{\cdot} y \in P \to (I \subseteq P \lor J \subseteq P)))$
8		raleq	$⊢ a = I \to (\forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P \leftrightarrow \forall x \in I \forall y \in b x \underset{˙}{\cdot} y \in P)$
9		sseq1	$⊢ a = I \to (a \subseteq P \leftrightarrow I \subseteq P)$
10	9	orbi1d	$⊢ a = I \to ((a \subseteq P \lor b \subseteq P) \leftrightarrow (I \subseteq P \lor b \subseteq P))$
11	8 10	imbi12d	$⊢ a = I \to ((\forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P \to (a \subseteq P \lor b \subseteq P)) \leftrightarrow (\forall x \in I \forall y \in b x \underset{˙}{\cdot} y \in P \to (I \subseteq P \lor b \subseteq P)))$
12	11	ralbidv	$⊢ a = I \to (\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)) \leftrightarrow \forall b \in LIdeal (R) (\forall x \in I \forall y \in b x \underset{˙}{\cdot} y \in P \to (I \subseteq P \lor b \subseteq P)))$
13	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))))$
14	13	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)))$
15	14	simp3d	$⊢ (R \in Ring \land P \in PrmIdeal (R)) \to \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))$
16	15	adantr	$⊢ ((R \in Ring \land P \in PrmIdeal (R)) \land (I \in LIdeal (R) \land J \in LIdeal (R))) \to \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))$
17		simprl	$⊢ ((R \in Ring \land P \in PrmIdeal (R)) \land (I \in LIdeal (R) \land J \in LIdeal (R))) \to I \in LIdeal (R)$
18	12 16 17	rspcdva	$⊢ ((R \in Ring \land P \in PrmIdeal (R)) \land (I \in LIdeal (R) \land J \in LIdeal (R))) \to \forall b \in LIdeal (R) (\forall x \in I \forall y \in b x \underset{˙}{\cdot} y \in P \to (I \subseteq P \lor b \subseteq P))$
19		simprr	$⊢ ((R \in Ring \land P \in PrmIdeal (R)) \land (I \in LIdeal (R) \land J \in LIdeal (R))) \to J \in LIdeal (R)$
20	7 18 19	rspcdva	$⊢ ((R \in Ring \land P \in PrmIdeal (R)) \land (I \in LIdeal (R) \land J \in LIdeal (R))) \to (\forall x \in I \forall y \in J x \underset{˙}{\cdot} y \in P \to (I \subseteq P \lor J \subseteq P))$
21	20	imp	$⊢ (((R \in Ring \land P \in PrmIdeal (R)) \land (I \in LIdeal (R) \land J \in LIdeal (R))) \land \forall x \in I \forall y \in J x \underset{˙}{\cdot} y \in P) \to (I \subseteq P \lor J \subseteq P)$

Metamath Proof Explorer

Theorem prmidl

Proof