zarclsiin

Description: In a Zariski topology, the intersection of the closures of a family of ideals is the closure of the span of their union. (Contributed by Thierry Arnoux, 16-Jun-2024)

	Ref	Expression
Hypotheses	zarclsx.1	$⊢ V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
	zarclsiin.1	$⊢ K = RSpan (R)$
Assertion	zarclsiin	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to ⋂_{l \in T} V (l) = V (K (⋃ T))$

Proof

Step	Hyp	Ref	Expression
1		zarclsx.1	$⊢ V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
2		zarclsiin.1	$⊢ K = RSpan (R)$
3		sseq2	$⊢ j = p \to (K (⋃ T) \subseteq j \leftrightarrow K (⋃ T) \subseteq p)$
4		simpl3	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to T \neq \emptyset$
5	1	a1i	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in T) \to V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
6		sseq1	$⊢ i = l \to (i \subseteq j \leftrightarrow l \subseteq j)$
7	6	rabbidv	$⊢ i = l \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| l \subseteq j\}$
8	7	adantl	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in T) \land i = l) \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| l \subseteq j\}$
9		simp2	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to T \subseteq LIdeal (R)$
10	9	sselda	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in T) \to l \in LIdeal (R)$
11		fvex	$⊢ PrmIdeal (R) \in V$
12	11	rabex	$⊢ \{j \in PrmIdeal (R) \| l \subseteq j\} \in V$
13	12	a1i	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in T) \to \{j \in PrmIdeal (R) \| l \subseteq j\} \in V$
14	5 8 10 13	fvmptd	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in T) \to V (l) = \{j \in PrmIdeal (R) \| l \subseteq j\}$
15		ssrab2	$⊢ \{j \in PrmIdeal (R) \| l \subseteq j\} \subseteq PrmIdeal (R)$
16	15	a1i	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in T) \to \{j \in PrmIdeal (R) \| l \subseteq j\} \subseteq PrmIdeal (R)$
17	14 16	eqsstrd	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in T) \to V (l) \subseteq PrmIdeal (R)$
18	17	sseld	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in T) \to (p \in V (l) \to p \in PrmIdeal (R))$
19	18	ralimdva	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to (\forall l \in T p \in V (l) \to \forall l \in T p \in PrmIdeal (R))$
20		eliin	$⊢ p \in V \to (p \in ⋂_{l \in T} V (l) \leftrightarrow \forall l \in T p \in V (l))$
21	20	elv	$⊢ p \in ⋂_{l \in T} V (l) \leftrightarrow \forall l \in T p \in V (l)$
22	21	biimpi	$⊢ p \in ⋂_{l \in T} V (l) \to \forall l \in T p \in V (l)$
23	19 22	impel	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to \forall l \in T p \in PrmIdeal (R)$
24		rspn0	$⊢ T \neq \emptyset \to (\forall l \in T p \in PrmIdeal (R) \to p \in PrmIdeal (R))$
25	24	imp	$⊢ (T \neq \emptyset \land \forall l \in T p \in PrmIdeal (R)) \to p \in PrmIdeal (R)$
26	4 23 25	syl2anc	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to p \in PrmIdeal (R)$
27		simp1	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to R \in Ring$
28	27	adantr	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to R \in Ring$
29		prmidlidl	$⊢ (R \in Ring \land p \in PrmIdeal (R)) \to p \in LIdeal (R)$
30	28 26 29	syl2anc	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to p \in LIdeal (R)$
31		nfv	$⊢ Ⅎ l (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset)$
32		nfcv	$⊢ \underline{Ⅎ} l p$
33		nfii1	$⊢ \underline{Ⅎ} l ⋂_{l \in T} V (l)$
34	32 33	nfel	$⊢ Ⅎ l p \in ⋂_{l \in T} V (l)$
35	31 34	nfan	$⊢ Ⅎ l ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l))$
36	22	a1i	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to (p \in ⋂_{l \in T} V (l) \to \forall l \in T p \in V (l))$
37	36	imp	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to \forall l \in T p \in V (l)$
38	37	adantr	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \land l \in T) \to \forall l \in T p \in V (l)$
39		simpr	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \land l \in T) \to l \in T$
40		rspa	$⊢ (\forall l \in T p \in V (l) \land l \in T) \to p \in V (l)$
41	38 39 40	syl2anc	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \land l \in T) \to p \in V (l)$
42	14	adantlr	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \land l \in T) \to V (l) = \{j \in PrmIdeal (R) \| l \subseteq j\}$
43	41 42	eleqtrd	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \land l \in T) \to p \in \{j \in PrmIdeal (R) \| l \subseteq j\}$
44		sseq2	$⊢ j = p \to (l \subseteq j \leftrightarrow l \subseteq p)$
45	44	elrab	$⊢ p \in \{j \in PrmIdeal (R) \| l \subseteq j\} \leftrightarrow (p \in PrmIdeal (R) \land l \subseteq p)$
46	43 45	sylib	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \land l \in T) \to (p \in PrmIdeal (R) \land l \subseteq p)$
47	46	simprd	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \land l \in T) \to l \subseteq p$
48	47	ex	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to (l \in T \to l \subseteq p)$
49	35 48	ralrimi	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to \forall l \in T l \subseteq p$
50		unissb	$⊢ ⋃ T \subseteq p \leftrightarrow \forall l \in T l \subseteq p$
51	49 50	sylibr	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to ⋃ T \subseteq p$
52		eqid	$⊢ LIdeal (R) = LIdeal (R)$
53	2 52	rspssp	$⊢ (R \in Ring \land p \in LIdeal (R) \land ⋃ T \subseteq p) \to K (⋃ T) \subseteq p$
54	28 30 51 53	syl3anc	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to K (⋃ T) \subseteq p$
55	3 26 54	elrabd	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to p \in \{j \in PrmIdeal (R) \| K (⋃ T) \subseteq j\}$
56	1	a1i	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
57		sseq1	$⊢ i = K (⋃ T) \to (i \subseteq j \leftrightarrow K (⋃ T) \subseteq j)$
58	57	rabbidv	$⊢ i = K (⋃ T) \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| K (⋃ T) \subseteq j\}$
59	58	adantl	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land i = K (⋃ T)) \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| K (⋃ T) \subseteq j\}$
60	9	sselda	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land i \in T) \to i \in LIdeal (R)$
61		eqid	$⊢ {Base}_{R} = {Base}_{R}$
62	61 52	lidlss	$⊢ i \in LIdeal (R) \to i \subseteq {Base}_{R}$
63	60 62	syl	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land i \in T) \to i \subseteq {Base}_{R}$
64	63	ralrimiva	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to \forall i \in T i \subseteq {Base}_{R}$
65		unissb	$⊢ ⋃ T \subseteq {Base}_{R} \leftrightarrow \forall i \in T i \subseteq {Base}_{R}$
66	64 65	sylibr	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to ⋃ T \subseteq {Base}_{R}$
67	2 61 52	rspcl	$⊢ (R \in Ring \land ⋃ T \subseteq {Base}_{R}) \to K (⋃ T) \in LIdeal (R)$
68	27 66 67	syl2anc	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to K (⋃ T) \in LIdeal (R)$
69	11	rabex	$⊢ \{j \in PrmIdeal (R) \| K (⋃ T) \subseteq j\} \in V$
70	69	a1i	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to \{j \in PrmIdeal (R) \| K (⋃ T) \subseteq j\} \in V$
71	56 59 68 70	fvmptd	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to V (K (⋃ T)) = \{j \in PrmIdeal (R) \| K (⋃ T) \subseteq j\}$
72	71	eleq2d	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to (p \in V (K (⋃ T)) \leftrightarrow p \in \{j \in PrmIdeal (R) \| K (⋃ T) \subseteq j\})$
73	72	adantr	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to (p \in V (K (⋃ T)) \leftrightarrow p \in \{j \in PrmIdeal (R) \| K (⋃ T) \subseteq j\})$
74	55 73	mpbird	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to p \in V (K (⋃ T))$
75	72	biimpa	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \to p \in \{j \in PrmIdeal (R) \| K (⋃ T) \subseteq j\}$
76	3	elrab	$⊢ p \in \{j \in PrmIdeal (R) \| K (⋃ T) \subseteq j\} \leftrightarrow (p \in PrmIdeal (R) \land K (⋃ T) \subseteq p)$
77	75 76	sylib	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \to (p \in PrmIdeal (R) \land K (⋃ T) \subseteq p)$
78	77	simpld	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \to p \in PrmIdeal (R)$
79	78	adantr	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to p \in PrmIdeal (R)$
80		elssuni	$⊢ l \in T \to l \subseteq ⋃ T$
81	80	adantl	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to l \subseteq ⋃ T$
82		simpll	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset)$
83	2 61	rspssid	$⊢ (R \in Ring \land ⋃ T \subseteq {Base}_{R}) \to ⋃ T \subseteq K (⋃ T)$
84	27 66 83	syl2anc	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to ⋃ T \subseteq K (⋃ T)$
85	82 84	syl	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to ⋃ T \subseteq K (⋃ T)$
86	81 85	sstrd	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to l \subseteq K (⋃ T)$
87	77	simprd	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \to K (⋃ T) \subseteq p$
88	87	adantr	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to K (⋃ T) \subseteq p$
89	86 88	sstrd	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to l \subseteq p$
90	44 79 89	elrabd	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to p \in \{j \in PrmIdeal (R) \| l \subseteq j\}$
91	9	adantr	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \to T \subseteq LIdeal (R)$
92	91	sselda	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to l \in LIdeal (R)$
93	1	a1i	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in LIdeal (R)) \to V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
94	7	adantl	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in LIdeal (R)) \land i = l) \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| l \subseteq j\}$
95		simpr	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in LIdeal (R)) \to l \in LIdeal (R)$
96	12	a1i	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in LIdeal (R)) \to \{j \in PrmIdeal (R) \| l \subseteq j\} \in V$
97	93 94 95 96	fvmptd	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in LIdeal (R)) \to V (l) = \{j \in PrmIdeal (R) \| l \subseteq j\}$
98	82 92 97	syl2anc	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to V (l) = \{j \in PrmIdeal (R) \| l \subseteq j\}$
99	90 98	eleqtrrd	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to p \in V (l)$
100	99	ralrimiva	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \to \forall l \in T p \in V (l)$
101	21	a1i	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \to (p \in ⋂_{l \in T} V (l) \leftrightarrow \forall l \in T p \in V (l))$
102	100 101	mpbird	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \to p \in ⋂_{l \in T} V (l)$
103	74 102	impbida	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to (p \in ⋂_{l \in T} V (l) \leftrightarrow p \in V (K (⋃ T)))$
104	103	eqrdv	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to ⋂_{l \in T} V (l) = V (K (⋃ T))$

Metamath Proof Explorer

Theorem zarclsiin

Proof