zarclssn

Description: The closed points of Zariski topology are the maximal ideals. (Contributed by Thierry Arnoux, 16-Jun-2024)

	Ref	Expression
Hypotheses	zarclsx.1	$⊢ V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
	zarclssn.1	$⊢ B = LIdeal (R)$
Assertion	zarclssn	$⊢ (R \in CRing \land M \in B) \to (\{M\} = V (M) \leftrightarrow M \in MaxIdeal (R))$

Proof

Step	Hyp	Ref	Expression
1		zarclsx.1	$⊢ V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
2		zarclssn.1	$⊢ B = LIdeal (R)$
3		crngring	$⊢ R \in CRing \to R \in Ring$
4	3	ad2antrr	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to R \in Ring$
5		simplr	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to M \in B$
6	5 2	eleqtrdi	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to M \in LIdeal (R)$
7		simpr	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to \{M\} = V (M)$
8	5	snn0d	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to \{M\} \neq \emptyset$
9	7 8	eqnetrrd	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to V (M) \neq \emptyset$
10		simpll	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to R \in CRing$
11		eqid	$⊢ {Base}_{R} = {Base}_{R}$
12	1 11	zarcls1	$⊢ (R \in CRing \land M \in LIdeal (R)) \to (V (M) = \emptyset \leftrightarrow M = {Base}_{R})$
13	12	necon3bid	$⊢ (R \in CRing \land M \in LIdeal (R)) \to (V (M) \neq \emptyset \leftrightarrow M \neq {Base}_{R})$
14	10 6 13	syl2anc	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to (V (M) \neq \emptyset \leftrightarrow M \neq {Base}_{R})$
15	9 14	mpbid	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to M \neq {Base}_{R}$
16		simpr	$⊢ (((((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \land m \in MaxIdeal (R)) \land j \subseteq m) \to j \subseteq m$
17	10	ad5antr	$⊢ (((((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \land m \in MaxIdeal (R)) \land j \subseteq m) \to R \in CRing$
18		simplr	$⊢ (((((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \land m \in MaxIdeal (R)) \land j \subseteq m) \to m \in MaxIdeal (R)$
19		eqid	$⊢ LSSum ({mulGrp}_{R}) = LSSum ({mulGrp}_{R})$
20	19	mxidlprm	$⊢ (R \in CRing \land m \in MaxIdeal (R)) \to m \in PrmIdeal (R)$
21	17 18 20	syl2anc	$⊢ (((((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \land m \in MaxIdeal (R)) \land j \subseteq m) \to m \in PrmIdeal (R)$
22		simp-4r	$⊢ (((((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \land m \in MaxIdeal (R)) \land j \subseteq m) \to M \subseteq j$
23	22 16	sstrd	$⊢ (((((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \land m \in MaxIdeal (R)) \land j \subseteq m) \to M \subseteq m$
24	1	a1i	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
25		sseq1	$⊢ i = M \to (i \subseteq j \leftrightarrow M \subseteq j)$
26	25	rabbidv	$⊢ i = M \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| M \subseteq j\}$
27	26	adantl	$⊢ (((R \in CRing \land M \in B) \land \{M\} = V (M)) \land i = M) \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| M \subseteq j\}$
28		fvex	$⊢ PrmIdeal (R) \in V$
29	28	rabex	$⊢ \{j \in PrmIdeal (R) \| M \subseteq j\} \in V$
30	29	a1i	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to \{j \in PrmIdeal (R) \| M \subseteq j\} \in V$
31	24 27 6 30	fvmptd	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to V (M) = \{j \in PrmIdeal (R) \| M \subseteq j\}$
32	7 31	eqtr2d	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to \{j \in PrmIdeal (R) \| M \subseteq j\} = \{M\}$
33		rabeqsn	$⊢ \{j \in PrmIdeal (R) \| M \subseteq j\} = \{M\} \leftrightarrow \forall j ((j \in PrmIdeal (R) \land M \subseteq j) \leftrightarrow j = M)$
34	32 33	sylib	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to \forall j ((j \in PrmIdeal (R) \land M \subseteq j) \leftrightarrow j = M)$
35	34	ad5antr	$⊢ (((((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \land m \in MaxIdeal (R)) \land j \subseteq m) \to \forall j ((j \in PrmIdeal (R) \land M \subseteq j) \leftrightarrow j = M)$
36		vex	$⊢ m \in V$
37		eleq1w	$⊢ j = m \to (j \in PrmIdeal (R) \leftrightarrow m \in PrmIdeal (R))$
38		sseq2	$⊢ j = m \to (M \subseteq j \leftrightarrow M \subseteq m)$
39	37 38	anbi12d	$⊢ j = m \to ((j \in PrmIdeal (R) \land M \subseteq j) \leftrightarrow (m \in PrmIdeal (R) \land M \subseteq m))$
40		eqeq1	$⊢ j = m \to (j = M \leftrightarrow m = M)$
41	39 40	bibi12d	$⊢ j = m \to (((j \in PrmIdeal (R) \land M \subseteq j) \leftrightarrow j = M) \leftrightarrow ((m \in PrmIdeal (R) \land M \subseteq m) \leftrightarrow m = M))$
42	36 41	spcv	$⊢ \forall j ((j \in PrmIdeal (R) \land M \subseteq j) \leftrightarrow j = M) \to ((m \in PrmIdeal (R) \land M \subseteq m) \leftrightarrow m = M)$
43	35 42	syl	$⊢ (((((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \land m \in MaxIdeal (R)) \land j \subseteq m) \to ((m \in PrmIdeal (R) \land M \subseteq m) \leftrightarrow m = M)$
44	21 23 43	mpbi2and	$⊢ (((((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \land m \in MaxIdeal (R)) \land j \subseteq m) \to m = M$
45	16 44	sseqtrd	$⊢ (((((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \land m \in MaxIdeal (R)) \land j \subseteq m) \to j \subseteq M$
46	45 22	eqssd	$⊢ (((((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \land m \in MaxIdeal (R)) \land j \subseteq m) \to j = M$
47	3	ad5antr	$⊢ (((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \to R \in Ring$
48		simpllr	$⊢ (((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \to j \in LIdeal (R)$
49		simpr	$⊢ (((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \to \neg j = {Base}_{R}$
50	49	neqned	$⊢ (((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \to j \neq {Base}_{R}$
51	11	ssmxidl	$⊢ (R \in Ring \land j \in LIdeal (R) \land j \neq {Base}_{R}) \to \exists m \in MaxIdeal (R) j \subseteq m$
52	47 48 50 51	syl3anc	$⊢ (((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \to \exists m \in MaxIdeal (R) j \subseteq m$
53	46 52	r19.29a	$⊢ (((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = {Base}_{R}) \to j = M$
54	53	ex	$⊢ ((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \to (\neg j = {Base}_{R} \to j = M)$
55	54	orrd	$⊢ ((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \to (j = {Base}_{R} \lor j = M)$
56	55	orcomd	$⊢ ((((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \land M \subseteq j) \to (j = M \lor j = {Base}_{R})$
57	56	ex	$⊢ (((R \in CRing \land M \in B) \land \{M\} = V (M)) \land j \in LIdeal (R)) \to (M \subseteq j \to (j = M \lor j = {Base}_{R}))$
58	57	ralrimiva	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to \forall j \in LIdeal (R) (M \subseteq j \to (j = M \lor j = {Base}_{R}))$
59	6 15 58	3jca	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to (M \in LIdeal (R) \land M \neq {Base}_{R} \land \forall j \in LIdeal (R) (M \subseteq j \to (j = M \lor j = {Base}_{R})))$
60	11	ismxidl	$⊢ R \in Ring \to (M \in MaxIdeal (R) \leftrightarrow (M \in LIdeal (R) \land M \neq {Base}_{R} \land \forall j \in LIdeal (R) (M \subseteq j \to (j = M \lor j = {Base}_{R}))))$
61	60	biimpar	$⊢ (R \in Ring \land (M \in LIdeal (R) \land M \neq {Base}_{R} \land \forall j \in LIdeal (R) (M \subseteq j \to (j = M \lor j = {Base}_{R})))) \to M \in MaxIdeal (R)$
62	4 59 61	syl2anc	$⊢ ((R \in CRing \land M \in B) \land \{M\} = V (M)) \to M \in MaxIdeal (R)$
63	1	a1i	$⊢ (R \in CRing \land M \in MaxIdeal (R)) \to V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
64	26	adantl	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land i = M) \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| M \subseteq j\}$
65	11	mxidlidl	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to M \in LIdeal (R)$
66	3 65	sylan	$⊢ (R \in CRing \land M \in MaxIdeal (R)) \to M \in LIdeal (R)$
67	29	a1i	$⊢ (R \in CRing \land M \in MaxIdeal (R)) \to \{j \in PrmIdeal (R) \| M \subseteq j\} \in V$
68	63 64 66 67	fvmptd	$⊢ (R \in CRing \land M \in MaxIdeal (R)) \to V (M) = \{j \in PrmIdeal (R) \| M \subseteq j\}$
69	3	ad2antrr	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land (j \in PrmIdeal (R) \land M \subseteq j)) \to R \in Ring$
70		simplr	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land (j \in PrmIdeal (R) \land M \subseteq j)) \to M \in MaxIdeal (R)$
71		simprl	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land (j \in PrmIdeal (R) \land M \subseteq j)) \to j \in PrmIdeal (R)$
72		prmidlidl	$⊢ (R \in Ring \land j \in PrmIdeal (R)) \to j \in LIdeal (R)$
73	69 71 72	syl2anc	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land (j \in PrmIdeal (R) \land M \subseteq j)) \to j \in LIdeal (R)$
74		simprr	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land (j \in PrmIdeal (R) \land M \subseteq j)) \to M \subseteq j$
75	73 74	jca	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land (j \in PrmIdeal (R) \land M \subseteq j)) \to (j \in LIdeal (R) \land M \subseteq j)$
76	11	mxidlmax	$⊢ ((R \in Ring \land M \in MaxIdeal (R)) \land (j \in LIdeal (R) \land M \subseteq j)) \to (j = M \lor j = {Base}_{R})$
77	69 70 75 76	syl21anc	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land (j \in PrmIdeal (R) \land M \subseteq j)) \to (j = M \lor j = {Base}_{R})$
78		eqid	$⊢ \cdot_{R} = \cdot_{R}$
79	11 78	prmidlnr	$⊢ (R \in Ring \land j \in PrmIdeal (R)) \to j \neq {Base}_{R}$
80	69 71 79	syl2anc	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land (j \in PrmIdeal (R) \land M \subseteq j)) \to j \neq {Base}_{R}$
81	80	neneqd	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land (j \in PrmIdeal (R) \land M \subseteq j)) \to \neg j = {Base}_{R}$
82	77 81	olcnd	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land (j \in PrmIdeal (R) \land M \subseteq j)) \to j = M$
83		simpr	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land j = M) \to j = M$
84	19	mxidlprm	$⊢ (R \in CRing \land M \in MaxIdeal (R)) \to M \in PrmIdeal (R)$
85	84	adantr	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land j = M) \to M \in PrmIdeal (R)$
86	83 85	eqeltrd	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land j = M) \to j \in PrmIdeal (R)$
87		ssidd	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land j = M) \to j \subseteq j$
88	83 87	eqsstrrd	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land j = M) \to M \subseteq j$
89	86 88	jca	$⊢ ((R \in CRing \land M \in MaxIdeal (R)) \land j = M) \to (j \in PrmIdeal (R) \land M \subseteq j)$
90	82 89	impbida	$⊢ (R \in CRing \land M \in MaxIdeal (R)) \to ((j \in PrmIdeal (R) \land M \subseteq j) \leftrightarrow j = M)$
91	90	alrimiv	$⊢ (R \in CRing \land M \in MaxIdeal (R)) \to \forall j ((j \in PrmIdeal (R) \land M \subseteq j) \leftrightarrow j = M)$
92	91 33	sylibr	$⊢ (R \in CRing \land M \in MaxIdeal (R)) \to \{j \in PrmIdeal (R) \| M \subseteq j\} = \{M\}$
93	68 92	eqtr2d	$⊢ (R \in CRing \land M \in MaxIdeal (R)) \to \{M\} = V (M)$
94	93	adantlr	$⊢ ((R \in CRing \land M \in B) \land M \in MaxIdeal (R)) \to \{M\} = V (M)$
95	62 94	impbida	$⊢ (R \in CRing \land M \in B) \to (\{M\} = V (M) \leftrightarrow M \in MaxIdeal (R))$

Metamath Proof Explorer

Theorem zarclssn

Proof