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 No typesetting found for |- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |-
Assertion zarclsint R CRing S ran V S S 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 CRing R Ring
3 2 ad4antr R CRing S ran V S r 𝒫 LIdeal R S = V r R Ring
4 elpwi r 𝒫 LIdeal R r LIdeal R
5 4 adantl R CRing S ran V S r 𝒫 LIdeal R r LIdeal R
6 5 adantr R CRing S ran V S r 𝒫 LIdeal R S = V r r LIdeal R
7 6 sselda R CRing S ran V S r 𝒫 LIdeal R S = V r i r i LIdeal R
8 eqid Base R = Base R
9 eqid LIdeal R = LIdeal R
10 8 9 lidlss i LIdeal R i Base R
11 7 10 syl R CRing S ran V S r 𝒫 LIdeal R S = V r i r i Base R
12 11 ralrimiva R CRing S ran V S r 𝒫 LIdeal R S = V r i r i Base R
13 unissb r Base R i r i Base R
14 12 13 sylibr R CRing S ran V S r 𝒫 LIdeal R S = V r r Base R
15 eqid RSpan R = RSpan R
16 15 8 9 rspcl R Ring r Base R RSpan R r LIdeal R
17 3 14 16 syl2anc R CRing S ran V S r 𝒫 LIdeal R S = V r RSpan R r LIdeal R
18 sseq1 i = RSpan R r i j RSpan R r 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 CRing S ran V S r 𝒫 LIdeal R S = V r S = V r
23 22 inteqd R CRing S ran V S r 𝒫 LIdeal R S = V r S = V r
24 1 funmpt2 Fun V
25 24 a1i R CRing S ran V S r 𝒫 LIdeal R S = V r 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 CRing S ran V S r 𝒫 LIdeal R S = V r r dom V
30 intimafv Fun V r dom V V r = l r V l
31 25 29 30 syl2anc R CRing S ran V S r 𝒫 LIdeal R S = V r V r = l r V l
32 23 31 eqtrd R CRing S ran V S r 𝒫 LIdeal R S = V r S = l r V l
33 simplr R CRing S ran V S r 𝒫 LIdeal R S = V r r = S = V r
34 simpr R CRing S ran V S r 𝒫 LIdeal R S = V r r = r =
35 34 imaeq2d R CRing S ran V S r 𝒫 LIdeal R S = V r r = V r = V
36 ima0 V =
37 35 36 eqtrdi R CRing S ran V S r 𝒫 LIdeal R S = V r r = V r =
38 33 37 eqtrd R CRing S ran V S r 𝒫 LIdeal R S = V r r = S =
39 simp-4r R CRing S ran V S r 𝒫 LIdeal R S = V r r = S
40 39 neneqd R CRing S ran V S r 𝒫 LIdeal R S = V r r = ¬ S =
41 38 40 pm2.65da R CRing S ran V S r 𝒫 LIdeal R S = V r ¬ r =
42 41 neqned R CRing S ran V S r 𝒫 LIdeal R S = V r r
43 1 15 zarclsiin R Ring r LIdeal R r l r V l = V RSpan R r
44 3 6 42 43 syl3anc R CRing S ran V S r 𝒫 LIdeal R S = V r l 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 S V
53 52 biimpi S S V
54 53 3ad2ant3 R CRing S ran V S S 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 CRing S ran V S r 𝒫 LIdeal R S = V r S ran V
59 fvexd R CRing S ran V S LIdeal R V
60 24 a1i R CRing S ran V S Fun V
61 simplr R CRing S ran V S S 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 CRing S ran V S S V LIdeal R
66 ssimaexg LIdeal R V Fun V S V LIdeal R r r LIdeal R S = V r
67 59 60 65 66 syl3anc R CRing S ran V S r r LIdeal R S = V r
68 vex r V
69 68 a1i R CRing S ran V S r LIdeal R r V
70 simpr R CRing S ran V S r LIdeal R r LIdeal R
71 69 70 elpwd R CRing S ran V S r LIdeal R r 𝒫 LIdeal R
72 71 ex R CRing S ran V S r LIdeal R r 𝒫 LIdeal R
73 72 anim1d R CRing S ran V S r LIdeal R S = V r r 𝒫 LIdeal R S = V r
74 73 eximdv R CRing S ran V S r r LIdeal R S = V r r r 𝒫 LIdeal R S = V r
75 67 74 mpd R CRing S ran V S r r 𝒫 LIdeal R S = V r
76 df-rex r 𝒫 LIdeal R S = V r r r 𝒫 LIdeal R S = V r
77 75 76 sylibr R CRing S ran V S r 𝒫 LIdeal R S = V r
78 58 77 r19.29a R CRing S ran V S S ran V
79 78 3impa R CRing S ran V S S ran V