prmidl2

Description: A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc for the equivalence in the commutative case. (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	prmidl2	$⊢ ((R \in Ring \land P \in LIdeal (R)) \land (P \neq B \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P)))) \to P \in PrmIdeal (R)$

Proof

Step	Hyp	Ref	Expression
1		prmidlval.1	$⊢ B = {Base}_{R}$
2		prmidlval.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		simpr	$⊢ (((((R \in Ring \land P \in LIdeal (R)) \land P \neq B) \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \land (a \in LIdeal (R) \land b \in LIdeal (R))) \land \forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P) \to \forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P$
4		simplrr	$⊢ (((((R \in Ring \land P \in LIdeal (R)) \land P \neq B) \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \land (a \in LIdeal (R) \land b \in LIdeal (R))) \land \forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P) \to b \in LIdeal (R)$
5		eqid	$⊢ LIdeal (R) = LIdeal (R)$
6	1 5	lidlss	$⊢ b \in LIdeal (R) \to b \subseteq B$
7	4 6	syl	$⊢ (((((R \in Ring \land P \in LIdeal (R)) \land P \neq B) \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \land (a \in LIdeal (R) \land b \in LIdeal (R))) \land \forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P) \to b \subseteq B$
8		simplrl	$⊢ (((((R \in Ring \land P \in LIdeal (R)) \land P \neq B) \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \land (a \in LIdeal (R) \land b \in LIdeal (R))) \land \forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P) \to a \in LIdeal (R)$
9	1 5	lidlss	$⊢ a \in LIdeal (R) \to a \subseteq B$
10	8 9	syl	$⊢ (((((R \in Ring \land P \in LIdeal (R)) \land P \neq B) \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \land (a \in LIdeal (R) \land b \in LIdeal (R))) \land \forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P) \to a \subseteq B$
11		simpllr	$⊢ (((((R \in Ring \land P \in LIdeal (R)) \land P \neq B) \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \land (a \in LIdeal (R) \land b \in LIdeal (R))) \land \forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P) \to \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))$
12		ssralv	$⊢ a \subseteq B \to (\forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P)) \to \forall x \in a \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P)))$
13	10 11 12	sylc	$⊢ (((((R \in Ring \land P \in LIdeal (R)) \land P \neq B) \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \land (a \in LIdeal (R) \land b \in LIdeal (R))) \land \forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P) \to \forall x \in a \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))$
14		ssralv	$⊢ b \subseteq B \to (\forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P)) \to \forall y \in b (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P)))$
15	14	ralimdv	$⊢ b \subseteq B \to (\forall x \in a \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P)) \to \forall x \in a \forall y \in b (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P)))$
16	7 13 15	sylc	$⊢ (((((R \in Ring \land P \in LIdeal (R)) \land P \neq B) \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \land (a \in LIdeal (R) \land b \in LIdeal (R))) \land \forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P) \to \forall x \in a \forall y \in b (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))$
17		r19.26-2	$⊢ \forall x \in a \forall y \in b (x \underset{˙}{\cdot} y \in P \land (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \leftrightarrow (\forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P \land \forall x \in a \forall y \in b (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P)))$
18		pm3.35	$⊢ (x \underset{˙}{\cdot} y \in P \land (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \to (x \in P \lor y \in P)$
19	18	2ralimi	$⊢ \forall x \in a \forall y \in b (x \underset{˙}{\cdot} y \in P \land (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \to \forall x \in a \forall y \in b (x \in P \lor y \in P)$
20	17 19	sylbir	$⊢ (\forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P \land \forall x \in a \forall y \in b (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \to \forall x \in a \forall y \in b (x \in P \lor y \in P)$
21	3 16 20	syl2anc	$⊢ (((((R \in Ring \land P \in LIdeal (R)) \land P \neq B) \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \land (a \in LIdeal (R) \land b \in LIdeal (R))) \land \forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P) \to \forall x \in a \forall y \in b (x \in P \lor y \in P)$
22		2ralor	$⊢ \forall x \in a \forall y \in b (x \in P \lor y \in P) \leftrightarrow (\forall x \in a x \in P \lor \forall y \in b y \in P)$
23		dfss3	$⊢ a \subseteq P \leftrightarrow \forall x \in a x \in P$
24		dfss3	$⊢ b \subseteq P \leftrightarrow \forall y \in b y \in P$
25	23 24	orbi12i	$⊢ (a \subseteq P \lor b \subseteq P) \leftrightarrow (\forall x \in a x \in P \lor \forall y \in b y \in P)$
26	22 25	sylbb2	$⊢ \forall x \in a \forall y \in b (x \in P \lor y \in P) \to (a \subseteq P \lor b \subseteq P)$
27	21 26	syl	$⊢ (((((R \in Ring \land P \in LIdeal (R)) \land P \neq B) \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \land (a \in LIdeal (R) \land b \in LIdeal (R))) \land \forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P) \to (a \subseteq P \lor b \subseteq P)$
28	27	ex	$⊢ ((((R \in Ring \land P \in LIdeal (R)) \land P \neq B) \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \land (a \in LIdeal (R) \land b \in LIdeal (R))) \to (\forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P \to (a \subseteq P \lor b \subseteq P))$
29	28	ralrimivva	$⊢ (((R \in Ring \land P \in LIdeal (R)) \land P \neq B) \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \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))$
30	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))))$
31	30	biimpar	$⊢ (R \in Ring \land (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)))) \to P \in PrmIdeal (R)$
32	31	3anassrs	$⊢ (((R \in Ring \land 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))) \to P \in PrmIdeal (R)$
33	29 32	syldan	$⊢ (((R \in Ring \land P \in LIdeal (R)) \land P \neq B) \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))) \to P \in PrmIdeal (R)$
34	33	anasss	$⊢ ((R \in Ring \land P \in LIdeal (R)) \land (P \neq B \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P)))) \to P \in PrmIdeal (R)$

Metamath Proof Explorer

Theorem prmidl2

Proof