zarcls1

Description: The unit ideal B is the only ideal whose closure in the Zariski topology is the empty set. Stronger form of the Proposition 1.1.2(i) of EGA p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024)

	Ref	Expression
Hypotheses	zarclsx.1	$⊢ V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
	zarcls1.1	$⊢ B = {Base}_{R}$
Assertion	zarcls1	$⊢ (R \in CRing \land I \in LIdeal (R)) \to (V (I) = \emptyset \leftrightarrow I = B)$

Proof

Step	Hyp	Ref	Expression
1		zarclsx.1	$⊢ V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
2		zarcls1.1	$⊢ B = {Base}_{R}$
3		simplr	$⊢ (((R \in CRing \land I \in LIdeal (R)) \land V (I) = \emptyset) \land I \neq B) \to V (I) = \emptyset$
4		sseq2	$⊢ j = m \to (I \subseteq j \leftrightarrow I \subseteq m)$
5		eqid	$⊢ LSSum ({mulGrp}_{R}) = LSSum ({mulGrp}_{R})$
6	5	mxidlprm	$⊢ (R \in CRing \land m \in MaxIdeal (R)) \to m \in PrmIdeal (R)$
7	6	ad5ant14	$⊢ ((((R \in CRing \land I \in LIdeal (R)) \land I \neq B) \land m \in MaxIdeal (R)) \land I \subseteq m) \to m \in PrmIdeal (R)$
8		simpr	$⊢ ((((R \in CRing \land I \in LIdeal (R)) \land I \neq B) \land m \in MaxIdeal (R)) \land I \subseteq m) \to I \subseteq m$
9	4 7 8	elrabd	$⊢ ((((R \in CRing \land I \in LIdeal (R)) \land I \neq B) \land m \in MaxIdeal (R)) \land I \subseteq m) \to m \in \{j \in PrmIdeal (R) \| I \subseteq j\}$
10	1	a1i	$⊢ ((((R \in CRing \land I \in LIdeal (R)) \land I \neq B) \land m \in MaxIdeal (R)) \land I \subseteq m) \to V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
11		sseq1	$⊢ i = I \to (i \subseteq j \leftrightarrow I \subseteq j)$
12	11	rabbidv	$⊢ i = I \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| I \subseteq j\}$
13	12	adantl	$⊢ (((((R \in CRing \land I \in LIdeal (R)) \land I \neq B) \land m \in MaxIdeal (R)) \land I \subseteq m) \land i = I) \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| I \subseteq j\}$
14		simp-4r	$⊢ ((((R \in CRing \land I \in LIdeal (R)) \land I \neq B) \land m \in MaxIdeal (R)) \land I \subseteq m) \to I \in LIdeal (R)$
15		fvex	$⊢ PrmIdeal (R) \in V$
16	15	rabex	$⊢ \{j \in PrmIdeal (R) \| I \subseteq j\} \in V$
17	16	a1i	$⊢ ((((R \in CRing \land I \in LIdeal (R)) \land I \neq B) \land m \in MaxIdeal (R)) \land I \subseteq m) \to \{j \in PrmIdeal (R) \| I \subseteq j\} \in V$
18	10 13 14 17	fvmptd	$⊢ ((((R \in CRing \land I \in LIdeal (R)) \land I \neq B) \land m \in MaxIdeal (R)) \land I \subseteq m) \to V (I) = \{j \in PrmIdeal (R) \| I \subseteq j\}$
19	9 18	eleqtrrd	$⊢ ((((R \in CRing \land I \in LIdeal (R)) \land I \neq B) \land m \in MaxIdeal (R)) \land I \subseteq m) \to m \in V (I)$
20		ne0i	$⊢ m \in V (I) \to V (I) \neq \emptyset$
21	19 20	syl	$⊢ ((((R \in CRing \land I \in LIdeal (R)) \land I \neq B) \land m \in MaxIdeal (R)) \land I \subseteq m) \to V (I) \neq \emptyset$
22		crngring	$⊢ R \in CRing \to R \in Ring$
23	2	ssmxidl	$⊢ (R \in Ring \land I \in LIdeal (R) \land I \neq B) \to \exists m \in MaxIdeal (R) I \subseteq m$
24	23	3expa	$⊢ ((R \in Ring \land I \in LIdeal (R)) \land I \neq B) \to \exists m \in MaxIdeal (R) I \subseteq m$
25	22 24	sylanl1	$⊢ ((R \in CRing \land I \in LIdeal (R)) \land I \neq B) \to \exists m \in MaxIdeal (R) I \subseteq m$
26	21 25	r19.29a	$⊢ ((R \in CRing \land I \in LIdeal (R)) \land I \neq B) \to V (I) \neq \emptyset$
27	26	adantlr	$⊢ (((R \in CRing \land I \in LIdeal (R)) \land V (I) = \emptyset) \land I \neq B) \to V (I) \neq \emptyset$
28	27	neneqd	$⊢ (((R \in CRing \land I \in LIdeal (R)) \land V (I) = \emptyset) \land I \neq B) \to \neg V (I) = \emptyset$
29	3 28	pm2.65da	$⊢ ((R \in CRing \land I \in LIdeal (R)) \land V (I) = \emptyset) \to \neg I \neq B$
30		nne	$⊢ \neg I \neq B \leftrightarrow I = B$
31	29 30	sylib	$⊢ ((R \in CRing \land I \in LIdeal (R)) \land V (I) = \emptyset) \to I = B$
32		fveq2	$⊢ I = B \to V (I) = V (B)$
33	32	adantl	$⊢ ((R \in CRing \land I \in LIdeal (R)) \land I = B) \to V (I) = V (B)$
34	1	a1i	$⊢ R \in Ring \to V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
35		sseq1	$⊢ i = B \to (i \subseteq j \leftrightarrow B \subseteq j)$
36	35	adantl	$⊢ (R \in Ring \land i = B) \to (i \subseteq j \leftrightarrow B \subseteq j)$
37	36	rabbidv	$⊢ (R \in Ring \land i = B) \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| B \subseteq j\}$
38		eqid	$⊢ LIdeal (R) = LIdeal (R)$
39	38 2	lidl1	$⊢ R \in Ring \to B \in LIdeal (R)$
40	15	rabex	$⊢ \{j \in PrmIdeal (R) \| B \subseteq j\} \in V$
41	40	a1i	$⊢ R \in Ring \to \{j \in PrmIdeal (R) \| B \subseteq j\} \in V$
42	34 37 39 41	fvmptd	$⊢ R \in Ring \to V (B) = \{j \in PrmIdeal (R) \| B \subseteq j\}$
43		prmidlidl	$⊢ (R \in Ring \land j \in PrmIdeal (R)) \to j \in LIdeal (R)$
44	2 38	lidlss	$⊢ j \in LIdeal (R) \to j \subseteq B$
45	43 44	syl	$⊢ (R \in Ring \land j \in PrmIdeal (R)) \to j \subseteq B$
46	45	adantr	$⊢ ((R \in Ring \land j \in PrmIdeal (R)) \land B \subseteq j) \to j \subseteq B$
47		simpr	$⊢ ((R \in Ring \land j \in PrmIdeal (R)) \land B \subseteq j) \to B \subseteq j$
48	46 47	eqssd	$⊢ ((R \in Ring \land j \in PrmIdeal (R)) \land B \subseteq j) \to j = B$
49		eqid	$⊢ \cdot_{R} = \cdot_{R}$
50	2 49	prmidlnr	$⊢ (R \in Ring \land j \in PrmIdeal (R)) \to j \neq B$
51	50	adantr	$⊢ ((R \in Ring \land j \in PrmIdeal (R)) \land B \subseteq j) \to j \neq B$
52	51	neneqd	$⊢ ((R \in Ring \land j \in PrmIdeal (R)) \land B \subseteq j) \to \neg j = B$
53	48 52	pm2.65da	$⊢ (R \in Ring \land j \in PrmIdeal (R)) \to \neg B \subseteq j$
54	53	ralrimiva	$⊢ R \in Ring \to \forall j \in PrmIdeal (R) \neg B \subseteq j$
55		rabeq0	$⊢ \{j \in PrmIdeal (R) \| B \subseteq j\} = \emptyset \leftrightarrow \forall j \in PrmIdeal (R) \neg B \subseteq j$
56	54 55	sylibr	$⊢ R \in Ring \to \{j \in PrmIdeal (R) \| B \subseteq j\} = \emptyset$
57	42 56	eqtrd	$⊢ R \in Ring \to V (B) = \emptyset$
58	22 57	syl	$⊢ R \in CRing \to V (B) = \emptyset$
59	58	ad2antrr	$⊢ ((R \in CRing \land I \in LIdeal (R)) \land I = B) \to V (B) = \emptyset$
60	33 59	eqtrd	$⊢ ((R \in CRing \land I \in LIdeal (R)) \land I = B) \to V (I) = \emptyset$
61	31 60	impbida	$⊢ (R \in CRing \land I \in LIdeal (R)) \to (V (I) = \emptyset \leftrightarrow I = B)$

Metamath Proof Explorer

Theorem zarcls1

Proof