zarclsint

Description: The intersection of a family of closed sets is closed in the Zariski topology. (Contributed by Thierry Arnoux, 16-Jun-2024)

		Ref	Expression
	Hypothesis	zarclsx.1	$⊢ V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
	Assertion	zarclsint	$⊢ (R \in CRing \land S \subseteq ran V \land S \neq \emptyset) \to ⋂ S \in ran V$

Proof

Step	Hyp	Ref	Expression
1		zarclsx.1	$⊢ V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
2		crngring	$⊢ R \in CRing \to R \in Ring$
3	2	ad4antr	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to R \in Ring$
4		elpwi	$⊢ r \in 𝒫 LIdeal (R) \to r \subseteq LIdeal (R)$
5	4	adantl	$⊢ (((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \to r \subseteq LIdeal (R)$
6	5	adantr	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to r \subseteq LIdeal (R)$
7	6	sselda	$⊢ (((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \land i \in r) \to i \in LIdeal (R)$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9		eqid	$⊢ LIdeal (R) = LIdeal (R)$
10	8 9	lidlss	$⊢ i \in LIdeal (R) \to i \subseteq {Base}_{R}$
11	7 10	syl	$⊢ (((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \land i \in r) \to i \subseteq {Base}_{R}$
12	11	ralrimiva	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to \forall i \in r i \subseteq {Base}_{R}$
13		unissb	$⊢ ⋃ r \subseteq {Base}_{R} \leftrightarrow \forall i \in r i \subseteq {Base}_{R}$
14	12 13	sylibr	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to ⋃ r \subseteq {Base}_{R}$
15		eqid	$⊢ RSpan (R) = RSpan (R)$
16	15 8 9	rspcl	$⊢ (R \in Ring \land ⋃ r \subseteq {Base}_{R}) \to RSpan (R) (⋃ r) \in LIdeal (R)$
17	3 14 16	syl2anc	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to RSpan (R) (⋃ r) \in LIdeal (R)$
18		sseq1	$⊢ i = RSpan (R) (⋃ r) \to (i \subseteq j \leftrightarrow RSpan (R) (⋃ r) \subseteq j)$
19	18	rabbidv	$⊢ i = RSpan (R) (⋃ r) \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| RSpan (R) (⋃ r) \subseteq j\}$
20	19	eqeq2d	$⊢ i = RSpan (R) (⋃ r) \to (⋂ S = \{j \in PrmIdeal (R) \| i \subseteq j\} \leftrightarrow ⋂ S = \{j \in PrmIdeal (R) \| RSpan (R) (⋃ r) \subseteq j\})$
21	20	adantl	$⊢ (((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \land i = RSpan (R) (⋃ r)) \to (⋂ S = \{j \in PrmIdeal (R) \| i \subseteq j\} \leftrightarrow ⋂ S = \{j \in PrmIdeal (R) \| RSpan (R) (⋃ r) \subseteq j\})$
22		simpr	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to S = V [r]$
23	22	inteqd	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to ⋂ S = ⋂ V [r]$
24	1	funmpt2	$⊢ Fun V$
25	24	a1i	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to Fun V$
26		fvex	$⊢ PrmIdeal (R) \in V$
27	26	rabex	$⊢ \{j \in PrmIdeal (R) \| i \subseteq j\} \in V$
28	27 1	dmmpti	$⊢ dom V = LIdeal (R)$
29	6 28	sseqtrrdi	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to r \subseteq dom V$
30		intimafv	$⊢ (Fun V \land r \subseteq dom V) \to ⋂ V [r] = ⋂_{l \in r} V (l)$
31	25 29 30	syl2anc	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to ⋂ V [r] = ⋂_{l \in r} V (l)$
32	23 31	eqtrd	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to ⋂ S = ⋂_{l \in r} V (l)$
33		simplr	$⊢ (((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \land r = \emptyset) \to S = V [r]$
34		simpr	$⊢ (((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \land r = \emptyset) \to r = \emptyset$
35	34	imaeq2d	$⊢ (((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \land r = \emptyset) \to V [r] = V [\emptyset]$
36		ima0	$⊢ V [\emptyset] = \emptyset$
37	35 36	eqtrdi	$⊢ (((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \land r = \emptyset) \to V [r] = \emptyset$
38	33 37	eqtrd	$⊢ (((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \land r = \emptyset) \to S = \emptyset$
39		simp-4r	$⊢ (((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \land r = \emptyset) \to S \neq \emptyset$
40	39	neneqd	$⊢ (((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \land r = \emptyset) \to \neg S = \emptyset$
41	38 40	pm2.65da	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to \neg r = \emptyset$
42	41	neqned	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to r \neq \emptyset$
43	1 15	zarclsiin	$⊢ (R \in Ring \land r \subseteq LIdeal (R) \land r \neq \emptyset) \to ⋂_{l \in r} V (l) = V (RSpan (R) (⋃ r))$
44	3 6 42 43	syl3anc	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to ⋂_{l \in r} V (l) = V (RSpan (R) (⋃ r))$
45	1	a1i	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
46	19	adantl	$⊢ (((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \land i = RSpan (R) (⋃ r)) \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| RSpan (R) (⋃ r) \subseteq j\}$
47	26	rabex	$⊢ \{j \in PrmIdeal (R) \| RSpan (R) (⋃ r) \subseteq j\} \in V$
48	47	a1i	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to \{j \in PrmIdeal (R) \| RSpan (R) (⋃ r) \subseteq j\} \in V$
49	45 46 17 48	fvmptd	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to V (RSpan (R) (⋃ r)) = \{j \in PrmIdeal (R) \| RSpan (R) (⋃ r) \subseteq j\}$
50	32 44 49	3eqtrd	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to ⋂ S = \{j \in PrmIdeal (R) \| RSpan (R) (⋃ r) \subseteq j\}$
51	17 21 50	rspcedvd	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to \exists i \in LIdeal (R) ⋂ S = \{j \in PrmIdeal (R) \| i \subseteq j\}$
52		intex	$⊢ S \neq \emptyset \leftrightarrow ⋂ S \in V$
53	52	biimpi	$⊢ S \neq \emptyset \to ⋂ S \in V$
54	53	3ad2ant3	$⊢ (R \in CRing \land S \subseteq ran V \land S \neq \emptyset) \to ⋂ S \in V$
55	1	elrnmpt	$⊢ ⋂ S \in V \to (⋂ S \in ran V \leftrightarrow \exists i \in LIdeal (R) ⋂ S = \{j \in PrmIdeal (R) \| i \subseteq j\})$
56	54 55	syl	$⊢ (R \in CRing \land S \subseteq ran V \land S \neq \emptyset) \to (⋂ S \in ran V \leftrightarrow \exists i \in LIdeal (R) ⋂ S = \{j \in PrmIdeal (R) \| i \subseteq j\})$
57	56	ad5ant123	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to (⋂ S \in ran V \leftrightarrow \exists i \in LIdeal (R) ⋂ S = \{j \in PrmIdeal (R) \| i \subseteq j\})$
58	51 57	mpbird	$⊢ ((((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \in 𝒫 LIdeal (R)) \land S = V [r]) \to ⋂ S \in ran V$
59		fvexd	$⊢ ((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \to LIdeal (R) \in V$
60	24	a1i	$⊢ ((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \to Fun V$
61		simplr	$⊢ ((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \to S \subseteq ran V$
62	27 1	fnmpti	$⊢ V Fn LIdeal (R)$
63		fnima	$⊢ V Fn LIdeal (R) \to V [LIdeal (R)] = ran V$
64	62 63	ax-mp	$⊢ V [LIdeal (R)] = ran V$
65	61 64	sseqtrrdi	$⊢ ((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \to S \subseteq V [LIdeal (R)]$
66		ssimaexg	$⊢ (LIdeal (R) \in V \land Fun V \land S \subseteq V [LIdeal (R)]) \to \exists r (r \subseteq LIdeal (R) \land S = V [r])$
67	59 60 65 66	syl3anc	$⊢ ((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \to \exists r (r \subseteq LIdeal (R) \land S = V [r])$
68		vex	$⊢ r \in V$
69	68	a1i	$⊢ (((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \subseteq LIdeal (R)) \to r \in V$
70		simpr	$⊢ (((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \subseteq LIdeal (R)) \to r \subseteq LIdeal (R)$
71	69 70	elpwd	$⊢ (((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \land r \subseteq LIdeal (R)) \to r \in 𝒫 LIdeal (R)$
72	71	ex	$⊢ ((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \to (r \subseteq LIdeal (R) \to r \in 𝒫 LIdeal (R))$
73	72	anim1d	$⊢ ((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \to ((r \subseteq LIdeal (R) \land S = V [r]) \to (r \in 𝒫 LIdeal (R) \land S = V [r]))$
74	73	eximdv	$⊢ ((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \to (\exists r (r \subseteq LIdeal (R) \land S = V [r]) \to \exists r (r \in 𝒫 LIdeal (R) \land S = V [r]))$
75	67 74	mpd	$⊢ ((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \to \exists r (r \in 𝒫 LIdeal (R) \land S = V [r])$
76		df-rex	$⊢ \exists r \in 𝒫 LIdeal (R) S = V [r] \leftrightarrow \exists r (r \in 𝒫 LIdeal (R) \land S = V [r])$
77	75 76	sylibr	$⊢ ((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \to \exists r \in 𝒫 LIdeal (R) S = V [r]$
78	58 77	r19.29a	$⊢ ((R \in CRing \land S \subseteq ran V) \land S \neq \emptyset) \to ⋂ S \in ran V$
79	78	3impa	$⊢ (R \in CRing \land S \subseteq ran V \land S \neq \emptyset) \to ⋂ S \in ran V$

Metamath Proof Explorer

Theorem zarclsint

Proof