isprmidlc

Description: The predicate "is prime ideal" for commutative rings. Alternate definition for commutative rings. See definition in Lang p. 92. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

	Ref	Expression
Hypotheses	isprmidlc.1	$⊢ B = {Base}_{R}$
	isprmidlc.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	isprmidlc	$⊢ R \in CRing \to (P \in PrmIdeal (R) \leftrightarrow (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))))$

Proof

Step	Hyp	Ref	Expression
1		isprmidlc.1	$⊢ B = {Base}_{R}$
2		isprmidlc.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		crngring	$⊢ R \in CRing \to R \in Ring$
4		prmidlidl	$⊢ (R \in Ring \land P \in PrmIdeal (R)) \to P \in LIdeal (R)$
5	3 4	sylan	$⊢ (R \in CRing \land P \in PrmIdeal (R)) \to P \in LIdeal (R)$
6	1 2	prmidlnr	$⊢ (R \in Ring \land P \in PrmIdeal (R)) \to P \neq B$
7	3 6	sylan	$⊢ (R \in CRing \land P \in PrmIdeal (R)) \to P \neq B$
8	3	ad4antr	$⊢ ((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \to R \in Ring$
9		simp-4r	$⊢ ((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \to P \in PrmIdeal (R)$
10		simpllr	$⊢ ((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \to x \in B$
11	10	snssd	$⊢ ((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \to \{x\} \subseteq B$
12		eqid	$⊢ RSpan (R) = RSpan (R)$
13		eqid	$⊢ LIdeal (R) = LIdeal (R)$
14	12 1 13	rspcl	$⊢ (R \in Ring \land \{x\} \subseteq B) \to RSpan (R) (\{x\}) \in LIdeal (R)$
15	8 11 14	syl2anc	$⊢ ((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \to RSpan (R) (\{x\}) \in LIdeal (R)$
16		simplr	$⊢ ((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \to y \in B$
17	16	snssd	$⊢ ((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \to \{y\} \subseteq B$
18	12 1 13	rspcl	$⊢ (R \in Ring \land \{y\} \subseteq B) \to RSpan (R) (\{y\}) \in LIdeal (R)$
19	8 17 18	syl2anc	$⊢ ((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \to RSpan (R) (\{y\}) \in LIdeal (R)$
20	15 19	jca	$⊢ ((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \to (RSpan (R) (\{x\}) \in LIdeal (R) \land RSpan (R) (\{y\}) \in LIdeal (R))$
21		simpllr	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to r = m \underset{˙}{\cdot} x$
22		simpr	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to s = n \underset{˙}{\cdot} y$
23	21 22	oveq12d	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to r \underset{˙}{\cdot} s = (m \underset{˙}{\cdot} x) \underset{˙}{\cdot} (n \underset{˙}{\cdot} y)$
24		simp-10l	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to R \in CRing$
25		simp-4r	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to m \in B$
26	10	ad2antrr	$⊢ ((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \to x \in B$
27	26	ad4antr	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to x \in B$
28		simplr	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to n \in B$
29	16	ad4antr	$⊢ ((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \to y \in B$
30	29	ad2antrr	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to y \in B$
31	1 2	cringm4	$⊢ (R \in CRing \land (m \in B \land x \in B) \land (n \in B \land y \in B)) \to (m \underset{˙}{\cdot} x) \underset{˙}{\cdot} (n \underset{˙}{\cdot} y) = (m \underset{˙}{\cdot} n) \underset{˙}{\cdot} (x \underset{˙}{\cdot} y)$
32	24 25 27 28 30 31	syl122anc	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to (m \underset{˙}{\cdot} x) \underset{˙}{\cdot} (n \underset{˙}{\cdot} y) = (m \underset{˙}{\cdot} n) \underset{˙}{\cdot} (x \underset{˙}{\cdot} y)$
33	24 3	syl	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to R \in Ring$
34	5	ad9antr	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to P \in LIdeal (R)$
35	1 2	ringcl	$⊢ (R \in Ring \land m \in B \land n \in B) \to m \underset{˙}{\cdot} n \in B$
36	33 25 28 35	syl3anc	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to m \underset{˙}{\cdot} n \in B$
37		simp-7r	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to x \underset{˙}{\cdot} y \in P$
38	13 1 2	lidlmcl	$⊢ ((R \in Ring \land P \in LIdeal (R)) \land (m \underset{˙}{\cdot} n \in B \land x \underset{˙}{\cdot} y \in P)) \to (m \underset{˙}{\cdot} n) \underset{˙}{\cdot} (x \underset{˙}{\cdot} y) \in P$
39	33 34 36 37 38	syl22anc	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to (m \underset{˙}{\cdot} n) \underset{˙}{\cdot} (x \underset{˙}{\cdot} y) \in P$
40	32 39	eqeltrd	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to (m \underset{˙}{\cdot} x) \underset{˙}{\cdot} (n \underset{˙}{\cdot} y) \in P$
41	23 40	eqeltrd	$⊢ ((((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \land n \in B) \land s = n \underset{˙}{\cdot} y) \to r \underset{˙}{\cdot} s \in P$
42	8	ad2antrr	$⊢ ((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \to R \in Ring$
43	42	ad2antrr	$⊢ ((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \to R \in Ring$
44		simpllr	$⊢ ((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \to s \in RSpan (R) (\{y\})$
45	1 2 12	elrspsn	$⊢ (R \in Ring \land y \in B) \to (s \in RSpan (R) (\{y\}) \leftrightarrow \exists n \in B s = n \underset{˙}{\cdot} y)$
46	45	biimpa	$⊢ ((R \in Ring \land y \in B) \land s \in RSpan (R) (\{y\})) \to \exists n \in B s = n \underset{˙}{\cdot} y$
47	43 29 44 46	syl21anc	$⊢ ((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \to \exists n \in B s = n \underset{˙}{\cdot} y$
48	41 47	r19.29a	$⊢ ((((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \land m \in B) \land r = m \underset{˙}{\cdot} x) \to r \underset{˙}{\cdot} s \in P$
49		simplr	$⊢ ((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \to r \in RSpan (R) (\{x\})$
50	1 2 12	elrspsn	$⊢ (R \in Ring \land x \in B) \to (r \in RSpan (R) (\{x\}) \leftrightarrow \exists m \in B r = m \underset{˙}{\cdot} x)$
51	50	biimpa	$⊢ ((R \in Ring \land x \in B) \land r \in RSpan (R) (\{x\})) \to \exists m \in B r = m \underset{˙}{\cdot} x$
52	42 26 49 51	syl21anc	$⊢ ((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \to \exists m \in B r = m \underset{˙}{\cdot} x$
53	48 52	r19.29a	$⊢ ((((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land r \in RSpan (R) (\{x\})) \land s \in RSpan (R) (\{y\})) \to r \underset{˙}{\cdot} s \in P$
54	53	anasss	$⊢ (((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \land (r \in RSpan (R) (\{x\}) \land s \in RSpan (R) (\{y\}))) \to r \underset{˙}{\cdot} s \in P$
55	54	ralrimivva	$⊢ ((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \to \forall r \in RSpan (R) (\{x\}) \forall s \in RSpan (R) (\{y\}) r \underset{˙}{\cdot} s \in P$
56	1 2	prmidl	$⊢ (((R \in Ring \land P \in PrmIdeal (R)) \land (RSpan (R) (\{x\}) \in LIdeal (R) \land RSpan (R) (\{y\}) \in LIdeal (R))) \land \forall r \in RSpan (R) (\{x\}) \forall s \in RSpan (R) (\{y\}) r \underset{˙}{\cdot} s \in P) \to (RSpan (R) (\{x\}) \subseteq P \lor RSpan (R) (\{y\}) \subseteq P)$
57	8 9 20 55 56	syl1111anc	$⊢ ((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \to (RSpan (R) (\{x\}) \subseteq P \lor RSpan (R) (\{y\}) \subseteq P)$
58	1 12	rspsnid	$⊢ (R \in Ring \land x \in B) \to x \in RSpan (R) (\{x\})$
59	3 58	sylan	$⊢ (R \in CRing \land x \in B) \to x \in RSpan (R) (\{x\})$
60	59	adantr	$⊢ ((R \in CRing \land x \in B) \land y \in B) \to x \in RSpan (R) (\{x\})$
61		ssel	$⊢ RSpan (R) (\{x\}) \subseteq P \to (x \in RSpan (R) (\{x\}) \to x \in P)$
62	60 61	syl5com	$⊢ ((R \in CRing \land x \in B) \land y \in B) \to (RSpan (R) (\{x\}) \subseteq P \to x \in P)$
63	1 12	rspsnid	$⊢ (R \in Ring \land y \in B) \to y \in RSpan (R) (\{y\})$
64	3 63	sylan	$⊢ (R \in CRing \land y \in B) \to y \in RSpan (R) (\{y\})$
65	64	adantlr	$⊢ ((R \in CRing \land x \in B) \land y \in B) \to y \in RSpan (R) (\{y\})$
66		ssel	$⊢ RSpan (R) (\{y\}) \subseteq P \to (y \in RSpan (R) (\{y\}) \to y \in P)$
67	65 66	syl5com	$⊢ ((R \in CRing \land x \in B) \land y \in B) \to (RSpan (R) (\{y\}) \subseteq P \to y \in P)$
68	62 67	orim12d	$⊢ ((R \in CRing \land x \in B) \land y \in B) \to ((RSpan (R) (\{x\}) \subseteq P \lor RSpan (R) (\{y\}) \subseteq P) \to (x \in P \lor y \in P))$
69	68	adantllr	$⊢ (((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \to ((RSpan (R) (\{x\}) \subseteq P \lor RSpan (R) (\{y\}) \subseteq P) \to (x \in P \lor y \in P))$
70	69	adantr	$⊢ ((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \to ((RSpan (R) (\{x\}) \subseteq P \lor RSpan (R) (\{y\}) \subseteq P) \to (x \in P \lor y \in P))$
71	57 70	mpd	$⊢ ((((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \land x \underset{˙}{\cdot} y \in P) \to (x \in P \lor y \in P)$
72	71	ex	$⊢ (((R \in CRing \land P \in PrmIdeal (R)) \land x \in B) \land y \in B) \to (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))$
73	72	anasss	$⊢ ((R \in CRing \land P \in PrmIdeal (R)) \land (x \in B \land y \in B)) \to (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))$
74	73	ralrimivva	$⊢ (R \in CRing \land P \in PrmIdeal (R)) \to \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y \in P \to (x \in P \lor y \in P))$
75	5 7 74	3jca	$⊢ (R \in CRing \land P \in PrmIdeal (R)) \to (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)))$
76		3anass	$⊢ (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))) \leftrightarrow (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))))$
77	1 2	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)$
78	77	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)$
79	76 78	sylan2b	$⊢ (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)$
80	3 79	sylan	$⊢ (R \in CRing \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)$
81	75 80	impbida	$⊢ R \in CRing \to (P \in PrmIdeal (R) \leftrightarrow (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))))$

Metamath Proof Explorer

Theorem isprmidlc

Proof