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	21	bilani	$⊢ ((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)$
37	36	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)$
38		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$
39		rspa	$⊢ (\forall l \in T p \in V (l) \land l \in T) \to p \in V (l)$
40	37 38 39	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)$
41	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\}$
42	40 41	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\}$
43		sseq2	$⊢ j = p \to (l \subseteq j \leftrightarrow l \subseteq p)$
44	43	elrab	$⊢ p \in \{j \in PrmIdeal (R) \| l \subseteq j\} \leftrightarrow (p \in PrmIdeal (R) \land l \subseteq p)$
45	42 44	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)$
46	45	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$
47	46	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)$
48	35 47	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$
49		unissb	$⊢ ⋃ T \subseteq p \leftrightarrow \forall l \in T l \subseteq p$
50	48 49	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$
51		eqid	$⊢ LIdeal (R) = LIdeal (R)$
52	2 51	rspssp	$⊢ (R \in Ring \land p \in LIdeal (R) \land ⋃ T \subseteq p) \to K (⋃ T) \subseteq p$
53	28 30 50 52	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$
54	3 26 53	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\}$
55	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\})$
56		sseq1	$⊢ i = K (⋃ T) \to (i \subseteq j \leftrightarrow K (⋃ T) \subseteq j)$
57	56	rabbidv	$⊢ i = K (⋃ T) \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| K (⋃ T) \subseteq j\}$
58	57	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\}$
59	9	sselda	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land i \in T) \to i \in LIdeal (R)$
60		eqid	$⊢ {Base}_{R} = {Base}_{R}$
61	60 51	lidlss	$⊢ i \in LIdeal (R) \to i \subseteq {Base}_{R}$
62	59 61	syl	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land i \in T) \to i \subseteq {Base}_{R}$
63	62	ralrimiva	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to \forall i \in T i \subseteq {Base}_{R}$
64		unissb	$⊢ ⋃ T \subseteq {Base}_{R} \leftrightarrow \forall i \in T i \subseteq {Base}_{R}$
65	63 64	sylibr	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to ⋃ T \subseteq {Base}_{R}$
66	2 60 51	rspcl	$⊢ (R \in Ring \land ⋃ T \subseteq {Base}_{R}) \to K (⋃ T) \in LIdeal (R)$
67	27 65 66	syl2anc	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to K (⋃ T) \in LIdeal (R)$
68	11	rabex	$⊢ \{j \in PrmIdeal (R) \| K (⋃ T) \subseteq j\} \in V$
69	68	a1i	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to \{j \in PrmIdeal (R) \| K (⋃ T) \subseteq j\} \in V$
70	55 58 67 69	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\}$
71	70	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\})$
72	71	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\})$
73	54 72	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))$
74	71	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\}$
75	3	elrab	$⊢ p \in \{j \in PrmIdeal (R) \| K (⋃ T) \subseteq j\} \leftrightarrow (p \in PrmIdeal (R) \land K (⋃ T) \subseteq p)$
76	74 75	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)$
77	76	simpld	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \to p \in PrmIdeal (R)$
78	77	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)$
79		elssuni	$⊢ l \in T \to l \subseteq ⋃ T$
80	79	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$
81		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)$
82	2 60	rspssid	$⊢ (R \in Ring \land ⋃ T \subseteq {Base}_{R}) \to ⋃ T \subseteq K (⋃ T)$
83	27 65 82	syl2anc	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to ⋃ T \subseteq K (⋃ T)$
84	81 83	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)$
85	80 84	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)$
86	76	simprd	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \to K (⋃ T) \subseteq p$
87	86	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$
88	85 87	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$
89	43 78 88	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\}$
90	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)$
91	90	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)$
92	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\})$
93	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\}$
94		simpr	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in LIdeal (R)) \to l \in LIdeal (R)$
95	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$
96	92 93 94 95	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\}$
97	81 91 96	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\}$
98	89 97	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)$
99	98	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)$
100	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))$
101	99 100	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)$
102	73 101	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)))$
103	102	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