Metamath Proof Explorer

Theorem 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 e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
zarclsiin.1 
|- K = ( RSpan ` R )
Assertion zarclsiin 
|- ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> |^|_ l e. T ( V ` l ) = ( V ` ( K ` U. T ) ) )

Proof

Step Hyp Ref Expression
1 zarclsx.1 
 |-  V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
2 zarclsiin.1 
 |-  K = ( RSpan ` R )
3 sseq2 
 |-  ( j = p -> ( ( K ` U. T ) C_ j <-> ( K ` U. T ) C_ p ) )
4 simpl3 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> T =/= (/) )
5 1 a1i 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) )
6 sseq1 
 |-  ( i = l -> ( i C_ j <-> l C_ j ) )
7 6 rabbidv 
 |-  ( i = l -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | l C_ j } )
8 7 adantl 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) /\ i = l ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | l C_ j } )
9 simp2 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> T C_ ( LIdeal ` R ) )
10 9 sselda 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> l e. ( LIdeal ` R ) )
11 fvex 
 |-  ( PrmIdeal ` R ) e. _V
12 11 rabex 
 |-  { j e. ( PrmIdeal ` R ) | l C_ j } e. _V
13 12 a1i 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> { j e. ( PrmIdeal ` R ) | l C_ j } e. _V )
14 5 8 10 13 fvmptd 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> ( V ` l ) = { j e. ( PrmIdeal ` R ) | l C_ j } )
15 ssrab2 
 |-  { j e. ( PrmIdeal ` R ) | l C_ j } C_ ( PrmIdeal ` R )
16 15 a1i 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> { j e. ( PrmIdeal ` R ) | l C_ j } C_ ( PrmIdeal ` R ) )
17 14 16 eqsstrd 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> ( V ` l ) C_ ( PrmIdeal ` R ) )
18 17 sseld 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> ( p e. ( V ` l ) -> p e. ( PrmIdeal ` R ) ) )
19 18 ralimdva 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> ( A. l e. T p e. ( V ` l ) -> A. l e. T p e. ( PrmIdeal ` R ) ) )
20 eliin 
 |-  ( p e. _V -> ( p e. |^|_ l e. T ( V ` l ) <-> A. l e. T p e. ( V ` l ) ) )
21 20 elv 
 |-  ( p e. |^|_ l e. T ( V ` l ) <-> A. l e. T p e. ( V ` l ) )
22 21 biimpi 
 |-  ( p e. |^|_ l e. T ( V ` l ) -> A. l e. T p e. ( V ` l ) )
23 19 22 impel 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> A. l e. T p e. ( PrmIdeal ` R ) )
24 rspn0 
 |-  ( T =/= (/) -> ( A. l e. T p e. ( PrmIdeal ` R ) -> p e. ( PrmIdeal ` R ) ) )
25 24 imp 
 |-  ( ( T =/= (/) /\ A. l e. T p e. ( PrmIdeal ` R ) ) -> p e. ( PrmIdeal ` R ) )
26 4 23 25 syl2anc 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> p e. ( PrmIdeal ` R ) )
27 simp1 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> R e. Ring )
28 27 adantr 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> R e. Ring )
29 prmidlidl 
 |-  ( ( R e. Ring /\ p e. ( PrmIdeal ` R ) ) -> p e. ( LIdeal ` R ) )
30 28 26 29 syl2anc 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> p e. ( LIdeal ` R ) )
31 nfv 
 |-  F/ l ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) )
32 nfcv 
 |-  F/_ l p
33 nfii1 
 |-  F/_ l |^|_ l e. T ( V ` l )
34 32 33 nfel 
 |-  F/ l p e. |^|_ l e. T ( V ` l )
35 31 34 nfan 
 |-  F/ l ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) )
36 22 a1i 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> ( p e. |^|_ l e. T ( V ` l ) -> A. l e. T p e. ( V ` l ) ) )
37 36 imp 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> A. l e. T p e. ( V ` l ) )
38 37 adantr 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) /\ l e. T ) -> A. l e. T p e. ( V ` l ) )
39 simpr 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) /\ l e. T ) -> l e. T )
40 rspa 
 |-  ( ( A. l e. T p e. ( V ` l ) /\ l e. T ) -> p e. ( V ` l ) )
41 38 39 40 syl2anc 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) /\ l e. T ) -> p e. ( V ` l ) )
42 14 adantlr 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) /\ l e. T ) -> ( V ` l ) = { j e. ( PrmIdeal ` R ) | l C_ j } )
43 41 42 eleqtrd 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) /\ l e. T ) -> p e. { j e. ( PrmIdeal ` R ) | l C_ j } )
44 sseq2 
 |-  ( j = p -> ( l C_ j <-> l C_ p ) )
45 44 elrab 
 |-  ( p e. { j e. ( PrmIdeal ` R ) | l C_ j } <-> ( p e. ( PrmIdeal ` R ) /\ l C_ p ) )
46 43 45 sylib 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) /\ l e. T ) -> ( p e. ( PrmIdeal ` R ) /\ l C_ p ) )
47 46 simprd 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) /\ l e. T ) -> l C_ p )
48 47 ex 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> ( l e. T -> l C_ p ) )
49 35 48 ralrimi 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> A. l e. T l C_ p )
50 unissb 
 |-  ( U. T C_ p <-> A. l e. T l C_ p )
51 49 50 sylibr 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> U. T C_ p )
52 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
53 2 52 rspssp 
 |-  ( ( R e. Ring /\ p e. ( LIdeal ` R ) /\ U. T C_ p ) -> ( K ` U. T ) C_ p )
54 28 30 51 53 syl3anc 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> ( K ` U. T ) C_ p )
55 3 26 54 elrabd 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> p e. { j e. ( PrmIdeal ` R ) | ( K ` U. T ) C_ j } )
56 1 a1i 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) )
57 sseq1 
 |-  ( i = ( K ` U. T ) -> ( i C_ j <-> ( K ` U. T ) C_ j ) )
58 57 rabbidv 
 |-  ( i = ( K ` U. T ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | ( K ` U. T ) C_ j } )
59 58 adantl 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ i = ( K ` U. T ) ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | ( K ` U. T ) C_ j } )
60 9 sselda 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ i e. T ) -> i e. ( LIdeal ` R ) )
61 eqid 
 |-  ( Base ` R ) = ( Base ` R )
62 61 52 lidlss 
 |-  ( i e. ( LIdeal ` R ) -> i C_ ( Base ` R ) )
63 60 62 syl 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ i e. T ) -> i C_ ( Base ` R ) )
64 63 ralrimiva 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> A. i e. T i C_ ( Base ` R ) )
65 unissb 
 |-  ( U. T C_ ( Base ` R ) <-> A. i e. T i C_ ( Base ` R ) )
66 64 65 sylibr 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> U. T C_ ( Base ` R ) )
67 2 61 52 rspcl 
 |-  ( ( R e. Ring /\ U. T C_ ( Base ` R ) ) -> ( K ` U. T ) e. ( LIdeal ` R ) )
68 27 66 67 syl2anc 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> ( K ` U. T ) e. ( LIdeal ` R ) )
69 11 rabex 
 |-  { j e. ( PrmIdeal ` R ) | ( K ` U. T ) C_ j } e. _V
70 69 a1i 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> { j e. ( PrmIdeal ` R ) | ( K ` U. T ) C_ j } e. _V )
71 56 59 68 70 fvmptd 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> ( V ` ( K ` U. T ) ) = { j e. ( PrmIdeal ` R ) | ( K ` U. T ) C_ j } )
72 71 eleq2d 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> ( p e. ( V ` ( K ` U. T ) ) <-> p e. { j e. ( PrmIdeal ` R ) | ( K ` U. T ) C_ j } ) )
73 72 adantr 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> ( p e. ( V ` ( K ` U. T ) ) <-> p e. { j e. ( PrmIdeal ` R ) | ( K ` U. T ) C_ j } ) )
74 55 73 mpbird 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> p e. ( V ` ( K ` U. T ) ) )
75 72 biimpa 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> p e. { j e. ( PrmIdeal ` R ) | ( K ` U. T ) C_ j } )
76 3 elrab 
 |-  ( p e. { j e. ( PrmIdeal ` R ) | ( K ` U. T ) C_ j } <-> ( p e. ( PrmIdeal ` R ) /\ ( K ` U. T ) C_ p ) )
77 75 76 sylib 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> ( p e. ( PrmIdeal ` R ) /\ ( K ` U. T ) C_ p ) )
78 77 simpld 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> p e. ( PrmIdeal ` R ) )
79 78 adantr 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> p e. ( PrmIdeal ` R ) )
80 elssuni 
 |-  ( l e. T -> l C_ U. T )
81 80 adantl 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> l C_ U. T )
82 simpll 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) )
83 2 61 rspssid 
 |-  ( ( R e. Ring /\ U. T C_ ( Base ` R ) ) -> U. T C_ ( K ` U. T ) )
84 27 66 83 syl2anc 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> U. T C_ ( K ` U. T ) )
85 82 84 syl 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> U. T C_ ( K ` U. T ) )
86 81 85 sstrd 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> l C_ ( K ` U. T ) )
87 77 simprd 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> ( K ` U. T ) C_ p )
88 87 adantr 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> ( K ` U. T ) C_ p )
89 86 88 sstrd 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> l C_ p )
90 44 79 89 elrabd 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> p e. { j e. ( PrmIdeal ` R ) | l C_ j } )
91 9 adantr 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> T C_ ( LIdeal ` R ) )
92 91 sselda 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> l e. ( LIdeal ` R ) )
93 1 a1i 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) )
94 7 adantl 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) /\ i = l ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | l C_ j } )
95 simpr 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) -> l e. ( LIdeal ` R ) )
96 12 a1i 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | l C_ j } e. _V )
97 93 94 95 96 fvmptd 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) -> ( V ` l ) = { j e. ( PrmIdeal ` R ) | l C_ j } )
98 82 92 97 syl2anc 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> ( V ` l ) = { j e. ( PrmIdeal ` R ) | l C_ j } )
99 90 98 eleqtrrd 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> p e. ( V ` l ) )
100 99 ralrimiva 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> A. l e. T p e. ( V ` l ) )
101 21 a1i 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> ( p e. |^|_ l e. T ( V ` l ) <-> A. l e. T p e. ( V ` l ) ) )
102 100 101 mpbird 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> p e. |^|_ l e. T ( V ` l ) )
103 74 102 impbida 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> ( p e. |^|_ l e. T ( V ` l ) <-> p e. ( V ` ( K ` U. T ) ) ) )
104 103 eqrdv 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> |^|_ l e. T ( V ` l ) = ( V ` ( K ` U. T ) ) )