Metamath Proof Explorer

Theorem zartopn

Description: The Zariski topology is a topology, and its closed sets are images by V of the ideals of R . (Contributed by Thierry Arnoux, 16-Jun-2024)

Ref Expression
Hypotheses zartop.1 
|- S = ( Spec ` R )
zartop.2 
|- J = ( TopOpen ` S )
zarcls.1 
|- P = ( PrmIdeal ` R )
zarcls.2 
|- V = ( i e. ( LIdeal ` R ) |-> { j e. P | i C_ j } )
Assertion zartopn 
|- ( R e. CRing -> ( J e. ( TopOn ` P ) /\ ran V = ( Clsd ` J ) ) )

Proof

Step Hyp Ref Expression
1 zartop.1 
 |-  S = ( Spec ` R )
2 zartop.2 
 |-  J = ( TopOpen ` S )
3 zarcls.1 
 |-  P = ( PrmIdeal ` R )
4 zarcls.2 
 |-  V = ( i e. ( LIdeal ` R ) |-> { j e. P | i C_ j } )
5 ssrab2 
 |-  { j e. P | i C_ j } C_ P
6 3 fvexi 
 |-  P e. _V
7 6 elpw2 
 |-  ( { j e. P | i C_ j } e. ~P P <-> { j e. P | i C_ j } C_ P )
8 5 7 mpbir 
 |-  { j e. P | i C_ j } e. ~P P
9 8 rgenw 
 |-  A. i e. ( LIdeal ` R ) { j e. P | i C_ j } e. ~P P
10 4 rnmptss 
 |-  ( A. i e. ( LIdeal ` R ) { j e. P | i C_ j } e. ~P P -> ran V C_ ~P P )
11 9 10 ax-mp 
 |-  ran V C_ ~P P
12 11 a1i 
 |-  ( R e. CRing -> ran V C_ ~P P )
13 crngring 
 |-  ( R e. CRing -> R e. Ring )
14 3 rabeqi 
 |-  { j e. P | i C_ j } = { j e. ( PrmIdeal ` R ) | i C_ j }
15 14 mpteq2i 
 |-  ( i e. ( LIdeal ` R ) |-> { j e. P | i C_ j } ) = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
16 4 15 eqtri 
 |-  V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
17 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
18 16 3 17 zarcls0 
 |-  ( R e. Ring -> ( V ` { ( 0g ` R ) } ) = P )
19 4 funmpt2 
 |-  Fun V
20 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
21 20 17 lidl0 
 |-  ( R e. Ring -> { ( 0g ` R ) } e. ( LIdeal ` R ) )
22 6 rabex 
 |-  { j e. P | i C_ j } e. _V
23 22 4 dmmpti 
 |-  dom V = ( LIdeal ` R )
24 21 23 eleqtrrdi 
 |-  ( R e. Ring -> { ( 0g ` R ) } e. dom V )
25 fvelrn 
 |-  ( ( Fun V /\ { ( 0g ` R ) } e. dom V ) -> ( V ` { ( 0g ` R ) } ) e. ran V )
26 19 24 25 sylancr 
 |-  ( R e. Ring -> ( V ` { ( 0g ` R ) } ) e. ran V )
27 18 26 eqeltrrd 
 |-  ( R e. Ring -> P e. ran V )
28 13 27 syl 
 |-  ( R e. CRing -> P e. ran V )
29 16 zarclsint 
 |-  ( ( R e. CRing /\ z C_ ran V /\ z =/= (/) ) -> |^| z e. ran V )
30 12 28 29 ismred 
 |-  ( R e. CRing -> ran V e. ( Moore ` P ) )
31 eqid 
 |-  ( Base ` R ) = ( Base ` R )
32 23 31 lidl1 
 |-  ( R e. Ring -> ( Base ` R ) e. dom V )
33 13 32 syl 
 |-  ( R e. CRing -> ( Base ` R ) e. dom V )
34 33 23 eleqtrdi 
 |-  ( R e. CRing -> ( Base ` R ) e. ( LIdeal ` R ) )
35 16 31 zarcls1 
 |-  ( ( R e. CRing /\ ( Base ` R ) e. ( LIdeal ` R ) ) -> ( ( V ` ( Base ` R ) ) = (/) <-> ( Base ` R ) = ( Base ` R ) ) )
36 31 35 mpbiri 
 |-  ( ( R e. CRing /\ ( Base ` R ) e. ( LIdeal ` R ) ) -> ( V ` ( Base ` R ) ) = (/) )
37 34 36 mpdan 
 |-  ( R e. CRing -> ( V ` ( Base ` R ) ) = (/) )
38 19 a1i 
 |-  ( R e. CRing -> Fun V )
39 fvelrn 
 |-  ( ( Fun V /\ ( Base ` R ) e. dom V ) -> ( V ` ( Base ` R ) ) e. ran V )
40 38 33 39 syl2anc 
 |-  ( R e. CRing -> ( V ` ( Base ` R ) ) e. ran V )
41 37 40 eqeltrrd 
 |-  ( R e. CRing -> (/) e. ran V )
42 16 zarclsun 
 |-  ( ( R e. CRing /\ x e. ran V /\ y e. ran V ) -> ( x u. y ) e. ran V )
43 eqid 
 |-  { s e. ~P P | ( P \ s ) e. ran V } = { s e. ~P P | ( P \ s ) e. ran V }
44 30 41 42 43 mretopd 
 |-  ( R e. CRing -> ( { s e. ~P P | ( P \ s ) e. ran V } e. ( TopOn ` P ) /\ ran V = ( Clsd ` { s e. ~P P | ( P \ s ) e. ran V } ) ) )
45 1 2 3 4 zarcls 
 |-  ( R e. Ring -> J = { s e. ~P P | ( P \ s ) e. ran V } )
46 13 45 syl 
 |-  ( R e. CRing -> J = { s e. ~P P | ( P \ s ) e. ran V } )
47 46 eleq1d 
 |-  ( R e. CRing -> ( J e. ( TopOn ` P ) <-> { s e. ~P P | ( P \ s ) e. ran V } e. ( TopOn ` P ) ) )
48 46 fveq2d 
 |-  ( R e. CRing -> ( Clsd ` J ) = ( Clsd ` { s e. ~P P | ( P \ s ) e. ran V } ) )
49 48 eqeq2d 
 |-  ( R e. CRing -> ( ran V = ( Clsd ` J ) <-> ran V = ( Clsd ` { s e. ~P P | ( P \ s ) e. ran V } ) ) )
50 47 49 anbi12d 
 |-  ( R e. CRing -> ( ( J e. ( TopOn ` P ) /\ ran V = ( Clsd ` J ) ) <-> ( { s e. ~P P | ( P \ s ) e. ran V } e. ( TopOn ` P ) /\ ran V = ( Clsd ` { s e. ~P P | ( P \ s ) e. ran V } ) ) ) )
51 44 50 mpbird 
 |-  ( R e. CRing -> ( J e. ( TopOn ` P ) /\ ran V = ( Clsd ` J ) ) )