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	Could not format assertion : No typesetting found for \|- ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ ( P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) -> P e. ( PrmIdeal ` R ) ) with typecode \|-

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	Could not format ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) ) : No typesetting found for \|- ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) ) with typecode \|-
31	30	biimpar	Could not format ( ( R e. Ring /\ ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) -> P e. ( PrmIdeal ` R ) ) : No typesetting found for \|- ( ( R e. Ring /\ ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) -> P e. ( PrmIdeal ` R ) ) with typecode \|-
32	31	3anassrs	Could not format ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) -> P e. ( PrmIdeal ` R ) ) : No typesetting found for \|- ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) -> P e. ( PrmIdeal ` R ) ) with typecode \|-
33	29 32	syldan	Could not format ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) -> P e. ( PrmIdeal ` R ) ) : No typesetting found for \|- ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) -> P e. ( PrmIdeal ` R ) ) with typecode \|-
34	33	anasss	Could not format ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ ( P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) -> P e. ( PrmIdeal ` R ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ ( P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) -> P e. ( PrmIdeal ` R ) ) with typecode \|-

Metamath Proof Explorer

Theorem prmidl2

Proof