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	No typesetting found for \|- V = ( i e. ( LIdeal ` R ) \|-> { j e. ( PrmIdeal ` R ) \| i C_ j } ) with typecode \|-
	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	Could not format V = ( i e. ( LIdeal ` R ) \|-> { j e. ( PrmIdeal ` R ) \| i C_ j } ) : No typesetting found for \|- V = ( i e. ( LIdeal ` R ) \|-> { j e. ( PrmIdeal ` R ) \| i C_ j } ) with typecode \|-
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	Could not format ( i = ( ( RSpan ` R ) ` U. r ) -> { j e. ( PrmIdeal ` R ) \| i C_ j } = { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } ) : No typesetting found for \|- ( i = ( ( RSpan ` R ) ` U. r ) -> { j e. ( PrmIdeal ` R ) \| i C_ j } = { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } ) with typecode \|-
20	19	eqeq2d	Could not format ( i = ( ( RSpan ` R ) ` U. r ) -> ( \|^\| S = { j e. ( PrmIdeal ` R ) \| i C_ j } <-> \|^\| S = { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } ) ) : No typesetting found for \|- ( i = ( ( RSpan ` R ) ` U. r ) -> ( \|^\| S = { j e. ( PrmIdeal ` R ) \| i C_ j } <-> \|^\| S = { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } ) ) with typecode \|-
21	20	adantl	Could not format ( ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) /\ i = ( ( RSpan ` R ) ` U. r ) ) -> ( \|^\| S = { j e. ( PrmIdeal ` R ) \| i C_ j } <-> \|^\| S = { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } ) ) : No typesetting found for \|- ( ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) /\ i = ( ( RSpan ` R ) ` U. r ) ) -> ( \|^\| S = { j e. ( PrmIdeal ` R ) \| i C_ j } <-> \|^\| S = { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } ) ) with typecode \|-
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	Could not format ( PrmIdeal ` R ) e. _V : No typesetting found for \|- ( PrmIdeal ` R ) e. _V with typecode \|-
27	26	rabex	Could not format { j e. ( PrmIdeal ` R ) \| i C_ j } e. _V : No typesetting found for \|- { j e. ( PrmIdeal ` R ) \| i C_ j } e. _V with typecode \|-
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	Could not format ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) -> V = ( i e. ( LIdeal ` R ) \|-> { j e. ( PrmIdeal ` R ) \| i C_ j } ) ) : No typesetting found for \|- ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) -> V = ( i e. ( LIdeal ` R ) \|-> { j e. ( PrmIdeal ` R ) \| i C_ j } ) ) with typecode \|-
46	19	adantl	Could not format ( ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) /\ i = ( ( RSpan ` R ) ` U. r ) ) -> { j e. ( PrmIdeal ` R ) \| i C_ j } = { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } ) : No typesetting found for \|- ( ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) /\ i = ( ( RSpan ` R ) ` U. r ) ) -> { j e. ( PrmIdeal ` R ) \| i C_ j } = { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } ) with typecode \|-
47	26	rabex	Could not format { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } e. _V : No typesetting found for \|- { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } e. _V with typecode \|-
48	47	a1i	Could not format ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) -> { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } e. _V ) : No typesetting found for \|- ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) -> { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } e. _V ) with typecode \|-
49	45 46 17 48	fvmptd	Could not format ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) -> ( V ` ( ( RSpan ` R ) ` U. r ) ) = { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } ) : No typesetting found for \|- ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) -> ( V ` ( ( RSpan ` R ) ` U. r ) ) = { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } ) with typecode \|-
50	32 44 49	3eqtrd	Could not format ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) -> \|^\| S = { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } ) : No typesetting found for \|- ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) -> \|^\| S = { j e. ( PrmIdeal ` R ) \| ( ( RSpan ` R ) ` U. r ) C_ j } ) with typecode \|-
51	17 21 50	rspcedvd	Could not format ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) -> E. i e. ( LIdeal ` R ) \|^\| S = { j e. ( PrmIdeal ` R ) \| i C_ j } ) : No typesetting found for \|- ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) -> E. i e. ( LIdeal ` R ) \|^\| S = { j e. ( PrmIdeal ` R ) \| i C_ j } ) with typecode \|-
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	Could not format ( \|^\| S e. _V -> ( \|^\| S e. ran V <-> E. i e. ( LIdeal ` R ) \|^\| S = { j e. ( PrmIdeal ` R ) \| i C_ j } ) ) : No typesetting found for \|- ( \|^\| S e. _V -> ( \|^\| S e. ran V <-> E. i e. ( LIdeal ` R ) \|^\| S = { j e. ( PrmIdeal ` R ) \| i C_ j } ) ) with typecode \|-
56	54 55	syl	Could not format ( ( R e. CRing /\ S C_ ran V /\ S =/= (/) ) -> ( \|^\| S e. ran V <-> E. i e. ( LIdeal ` R ) \|^\| S = { j e. ( PrmIdeal ` R ) \| i C_ j } ) ) : No typesetting found for \|- ( ( R e. CRing /\ S C_ ran V /\ S =/= (/) ) -> ( \|^\| S e. ran V <-> E. i e. ( LIdeal ` R ) \|^\| S = { j e. ( PrmIdeal ` R ) \| i C_ j } ) ) with typecode \|-
57	56	ad5ant123	Could not format ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) -> ( \|^\| S e. ran V <-> E. i e. ( LIdeal ` R ) \|^\| S = { j e. ( PrmIdeal ` R ) \| i C_ j } ) ) : No typesetting found for \|- ( ( ( ( ( R e. CRing /\ S C_ ran V ) /\ S =/= (/) ) /\ r e. ~P ( LIdeal ` R ) ) /\ S = ( V " r ) ) -> ( \|^\| S e. ran V <-> E. i e. ( LIdeal ` R ) \|^\| S = { j e. ( PrmIdeal ` R ) \| i C_ j } ) ) with typecode \|-
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