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 21 bilani 
 |-  ( ( ( 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 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 ) )
38 simpr 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) /\ l e. T ) -> l e. T )
39 rspa 
 |-  ( ( A. l e. T p e. ( V ` l ) /\ l e. T ) -> p e. ( V ` l ) )
40 37 38 39 syl2anc 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) /\ l e. T ) -> p e. ( V ` l ) )
41 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 } )
42 40 41 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 } )
43 sseq2 
 |-  ( j = p -> ( l C_ j <-> l C_ p ) )
44 43 elrab 
 |-  ( p e. { j e. ( PrmIdeal ` R ) | l C_ j } <-> ( p e. ( PrmIdeal ` R ) /\ l C_ p ) )
45 42 44 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 ) )
46 45 simprd 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) /\ l e. T ) -> l C_ p )
47 46 ex 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> ( l e. T -> l C_ p ) )
48 35 47 ralrimi 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> A. l e. T l C_ p )
49 unissb 
 |-  ( U. T C_ p <-> A. l e. T l C_ p )
50 48 49 sylibr 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> U. T C_ p )
51 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
52 2 51 rspssp 
 |-  ( ( R e. Ring /\ p e. ( LIdeal ` R ) /\ U. T C_ p ) -> ( K ` U. T ) C_ p )
53 28 30 50 52 syl3anc 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> ( K ` U. T ) C_ p )
54 3 26 53 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 } )
55 1 a1i 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) )
56 sseq1 
 |-  ( i = ( K ` U. T ) -> ( i C_ j <-> ( K ` U. T ) C_ j ) )
57 56 rabbidv 
 |-  ( i = ( K ` U. T ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | ( K ` U. T ) C_ j } )
58 57 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 } )
59 9 sselda 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ i e. T ) -> i e. ( LIdeal ` R ) )
60 eqid 
 |-  ( Base ` R ) = ( Base ` R )
61 60 51 lidlss 
 |-  ( i e. ( LIdeal ` R ) -> i C_ ( Base ` R ) )
62 59 61 syl 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ i e. T ) -> i C_ ( Base ` R ) )
63 62 ralrimiva 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> A. i e. T i C_ ( Base ` R ) )
64 unissb 
 |-  ( U. T C_ ( Base ` R ) <-> A. i e. T i C_ ( Base ` R ) )
65 63 64 sylibr 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> U. T C_ ( Base ` R ) )
66 2 60 51 rspcl 
 |-  ( ( R e. Ring /\ U. T C_ ( Base ` R ) ) -> ( K ` U. T ) e. ( LIdeal ` R ) )
67 27 65 66 syl2anc 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> ( K ` U. T ) e. ( LIdeal ` R ) )
68 11 rabex 
 |-  { j e. ( PrmIdeal ` R ) | ( K ` U. T ) C_ j } e. _V
69 68 a1i 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> { j e. ( PrmIdeal ` R ) | ( K ` U. T ) C_ j } e. _V )
70 55 58 67 69 fvmptd 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> ( V ` ( K ` U. T ) ) = { j e. ( PrmIdeal ` R ) | ( K ` U. T ) C_ j } )
71 70 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 } ) )
72 71 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 } ) )
73 54 72 mpbird 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. |^|_ l e. T ( V ` l ) ) -> p e. ( V ` ( K ` U. T ) ) )
74 71 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 } )
75 3 elrab 
 |-  ( p e. { j e. ( PrmIdeal ` R ) | ( K ` U. T ) C_ j } <-> ( p e. ( PrmIdeal ` R ) /\ ( K ` U. T ) C_ p ) )
76 74 75 sylib 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> ( p e. ( PrmIdeal ` R ) /\ ( K ` U. T ) C_ p ) )
77 76 simpld 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> p e. ( PrmIdeal ` R ) )
78 77 adantr 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> p e. ( PrmIdeal ` R ) )
79 elssuni 
 |-  ( l e. T -> l C_ U. T )
80 79 adantl 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> l C_ U. T )
81 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 =/= (/) ) )
82 2 60 rspssid 
 |-  ( ( R e. Ring /\ U. T C_ ( Base ` R ) ) -> U. T C_ ( K ` U. T ) )
83 27 65 82 syl2anc 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> U. T C_ ( K ` U. T ) )
84 81 83 syl 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> U. T C_ ( K ` U. T ) )
85 80 84 sstrd 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> l C_ ( K ` U. T ) )
86 76 simprd 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> ( K ` U. T ) C_ p )
87 86 adantr 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> ( K ` U. T ) C_ p )
88 85 87 sstrd 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> l C_ p )
89 43 78 88 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 } )
90 9 adantr 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> T C_ ( LIdeal ` R ) )
91 90 sselda 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> l e. ( LIdeal ` R ) )
92 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 } ) )
93 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 } )
94 simpr 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) -> l e. ( LIdeal ` R ) )
95 12 a1i 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | l C_ j } e. _V )
96 92 93 94 95 fvmptd 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) -> ( V ` l ) = { j e. ( PrmIdeal ` R ) | l C_ j } )
97 81 91 96 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 } )
98 89 97 eleqtrrd 
 |-  ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> p e. ( V ` l ) )
99 98 ralrimiva 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> A. l e. T p e. ( V ` l ) )
100 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 ) ) )
101 99 100 mpbird 
 |-  ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> p e. |^|_ l e. T ( V ` l ) )
102 73 101 impbida 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> ( p e. |^|_ l e. T ( V ` l ) <-> p e. ( V ` ( K ` U. T ) ) ) )
103 102 eqrdv 
 |-  ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> |^|_ l e. T ( V ` l ) = ( V ` ( K ` U. T ) ) )