Metamath Proof Explorer

Theorem zarclsun

Description: The union of two closed sets of the Zariski topology is closed. (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 zarclsun 
|- ( ( R e. CRing /\ X e. ran V /\ Y e. ran V ) -> ( X u. Y ) e. ran V )

Proof

Step Hyp Ref Expression
1 zarclsx.1 
 |-  V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
2 simpllr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> X = { j e. ( PrmIdeal ` R ) | l C_ j } )
3 simpr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> Y = { j e. ( PrmIdeal ` R ) | k C_ j } )
4 2 3 uneq12d 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> ( X u. Y ) = ( { j e. ( PrmIdeal ` R ) | l C_ j } u. { j e. ( PrmIdeal ` R ) | k C_ j } ) )
5 unrab 
 |-  ( { j e. ( PrmIdeal ` R ) | l C_ j } u. { j e. ( PrmIdeal ` R ) | k C_ j } ) = { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) }
6 eqid 
 |-  ( IDLsrg ` R ) = ( IDLsrg ` R )
7 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
8 eqid 
 |-  ( .r ` ( IDLsrg ` R ) ) = ( .r ` ( IDLsrg ` R ) )
9 simpll 
 |-  ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> R e. CRing )
10 9 crngringd 
 |-  ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> R e. Ring )
11 simplr 
 |-  ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> l e. ( LIdeal ` R ) )
12 simpr 
 |-  ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> k e. ( LIdeal ` R ) )
13 6 7 8 10 11 12 idlsrgmulrcl 
 |-  ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) e. ( LIdeal ` R ) )
14 sseq1 
 |-  ( i = ( l ( .r ` ( IDLsrg ` R ) ) k ) -> ( i C_ j <-> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) )
15 14 rabbidv 
 |-  ( i = ( l ( .r ` ( IDLsrg ` R ) ) k ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j } )
16 15 eqeq2d 
 |-  ( i = ( l ( .r ` ( IDLsrg ` R ) ) k ) -> ( { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | i C_ j } <-> { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j } ) )
17 16 adantl 
 |-  ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ i = ( l ( .r ` ( IDLsrg ` R ) ) k ) ) -> ( { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | i C_ j } <-> { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j } ) )
18 eqid 
 |-  ( .r ` R ) = ( .r ` R )
19 9 ad2antrr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> R e. CRing )
20 11 ad2antrr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> l e. ( LIdeal ` R ) )
21 12 ad2antrr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> k e. ( LIdeal ` R ) )
22 6 7 8 18 19 20 21 idlsrgmulrss1 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ l )
23 simpr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> l C_ j )
24 22 23 sstrd 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j )
25 10 ad2antrr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> R e. Ring )
26 11 ad2antrr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> l e. ( LIdeal ` R ) )
27 12 ad2antrr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> k e. ( LIdeal ` R ) )
28 6 7 8 18 25 26 27 idlsrgmulrss2 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ k )
29 simpr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> k C_ j )
30 28 29 sstrd 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j )
31 24 30 jaodan 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l C_ j \/ k C_ j ) ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j )
32 eqid 
 |-  ( LSSum ` ( mulGrp ` R ) ) = ( LSSum ` ( mulGrp ` R ) )
33 10 ad2antrr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> R e. Ring )
34 simplr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> j e. ( PrmIdeal ` R ) )
35 11 ad2antrr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> l e. ( LIdeal ` R ) )
36 12 ad2antrr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> k e. ( LIdeal ` R ) )
37 eqid 
 |-  ( Base ` R ) = ( Base ` R )
38 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
39 37 7 lidlss 
 |-  ( l e. ( LIdeal ` R ) -> l C_ ( Base ` R ) )
40 35 39 syl 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> l C_ ( Base ` R ) )
41 37 7 lidlss 
 |-  ( k e. ( LIdeal ` R ) -> k C_ ( Base ` R ) )
42 36 41 syl 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> k C_ ( Base ` R ) )
43 37 38 32 33 40 42 ringlsmss 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( LSSum ` ( mulGrp ` R ) ) k ) C_ ( Base ` R ) )
44 eqid 
 |-  ( RSpan ` R ) = ( RSpan ` R )
45 44 37 rspssid 
 |-  ( ( R e. Ring /\ ( l ( LSSum ` ( mulGrp ` R ) ) k ) C_ ( Base ` R ) ) -> ( l ( LSSum ` ( mulGrp ` R ) ) k ) C_ ( ( RSpan ` R ) ` ( l ( LSSum ` ( mulGrp ` R ) ) k ) ) )
46 33 43 45 syl2anc 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( LSSum ` ( mulGrp ` R ) ) k ) C_ ( ( RSpan ` R ) ` ( l ( LSSum ` ( mulGrp ` R ) ) k ) ) )
47 6 7 8 38 32 33 35 36 idlsrgmulrval 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) = ( ( RSpan ` R ) ` ( l ( LSSum ` ( mulGrp ` R ) ) k ) ) )
48 46 47 sseqtrrd 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( LSSum ` ( mulGrp ` R ) ) k ) C_ ( l ( .r ` ( IDLsrg ` R ) ) k ) )
49 simpr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j )
50 48 49 sstrd 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( LSSum ` ( mulGrp ` R ) ) k ) C_ j )
51 32 33 34 35 36 50 idlmulssprm 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l C_ j \/ k C_ j ) )
52 31 51 impbida 
 |-  ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) -> ( ( l C_ j \/ k C_ j ) <-> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) )
53 52 rabbidva 
 |-  ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j } )
54 13 17 53 rspcedvd 
 |-  ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> E. i e. ( LIdeal ` R ) { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | i C_ j } )
55 fvex 
 |-  ( PrmIdeal ` R ) e. _V
56 55 rabex 
 |-  { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } e. _V
57 56 a1i 
 |-  ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } e. _V )
58 1 54 57 elrnmptd 
 |-  ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } e. ran V )
59 5 58 eqeltrid 
 |-  ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> ( { j e. ( PrmIdeal ` R ) | l C_ j } u. { j e. ( PrmIdeal ` R ) | k C_ j } ) e. ran V )
60 59 adantlr 
 |-  ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) -> ( { j e. ( PrmIdeal ` R ) | l C_ j } u. { j e. ( PrmIdeal ` R ) | k C_ j } ) e. ran V )
61 60 adantr 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> ( { j e. ( PrmIdeal ` R ) | l C_ j } u. { j e. ( PrmIdeal ` R ) | k C_ j } ) e. ran V )
62 4 61 eqeltrd 
 |-  ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> ( X u. Y ) e. ran V )
63 62 adantl4r 
 |-  ( ( ( ( ( ( R e. CRing /\ Y e. ran V ) /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> ( X u. Y ) e. ran V )
64 55 rabex 
 |-  { j e. ( PrmIdeal ` R ) | i C_ j } e. _V
65 1 64 elrnmpti 
 |-  ( Y e. ran V <-> E. i e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | i C_ j } )
66 sseq1 
 |-  ( i = k -> ( i C_ j <-> k C_ j ) )
67 66 rabbidv 
 |-  ( i = k -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | k C_ j } )
68 67 eqeq2d 
 |-  ( i = k -> ( Y = { j e. ( PrmIdeal ` R ) | i C_ j } <-> Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) )
69 68 cbvrexvw 
 |-  ( E. i e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | i C_ j } <-> E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } )
70 biid 
 |-  ( E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } <-> E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } )
71 65 69 70 3bitri 
 |-  ( Y e. ran V <-> E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } )
72 71 biimpi 
 |-  ( Y e. ran V -> E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } )
73 72 ad3antlr 
 |-  ( ( ( ( R e. CRing /\ Y e. ran V ) /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) -> E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } )
74 63 73 r19.29a 
 |-  ( ( ( ( R e. CRing /\ Y e. ran V ) /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) -> ( X u. Y ) e. ran V )
75 74 adantl3r 
 |-  ( ( ( ( ( R e. CRing /\ X e. ran V ) /\ Y e. ran V ) /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) -> ( X u. Y ) e. ran V )
76 1 64 elrnmpti 
 |-  ( X e. ran V <-> E. i e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | i C_ j } )
77 sseq1 
 |-  ( i = l -> ( i C_ j <-> l C_ j ) )
78 77 rabbidv 
 |-  ( i = l -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | l C_ j } )
79 78 eqeq2d 
 |-  ( i = l -> ( X = { j e. ( PrmIdeal ` R ) | i C_ j } <-> X = { j e. ( PrmIdeal ` R ) | l C_ j } ) )
80 79 cbvrexvw 
 |-  ( E. i e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | i C_ j } <-> E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } )
81 biid 
 |-  ( E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } <-> E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } )
82 76 80 81 3bitri 
 |-  ( X e. ran V <-> E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } )
83 82 biimpi 
 |-  ( X e. ran V -> E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } )
84 83 ad2antlr 
 |-  ( ( ( R e. CRing /\ X e. ran V ) /\ Y e. ran V ) -> E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } )
85 75 84 r19.29a 
 |-  ( ( ( R e. CRing /\ X e. ran V ) /\ Y e. ran V ) -> ( X u. Y ) e. ran V )
86 85 3impa 
 |-  ( ( R e. CRing /\ X e. ran V /\ Y e. ran V ) -> ( X u. Y ) e. ran V )