Metamath Proof Explorer

Theorem 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 e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
Assertion zarclsint 
|- ( ( R e. CRing /\ S C_ ran V /\ S =/= (/) ) -> |^| S e. ran V )

Proof

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