Metamath Proof Explorer


Theorem zarcls0

Description: The closure of the identity ideal in the Zariski topology. Proposition 1.1.2(i) of EGA p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024)

Ref Expression
Hypotheses zarclsx.1
|- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
zarcls0.1
|- P = ( PrmIdeal ` R )
zarcls0.2
|- .0. = ( 0g ` R )
Assertion zarcls0
|- ( R e. Ring -> ( V ` { .0. } ) = P )

Proof

Step Hyp Ref Expression
1 zarclsx.1
 |-  V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
2 zarcls0.1
 |-  P = ( PrmIdeal ` R )
3 zarcls0.2
 |-  .0. = ( 0g ` R )
4 1 a1i
 |-  ( R e. Ring -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) )
5 simplr
 |-  ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> i = { .0. } )
6 simpll
 |-  ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> R e. Ring )
7 prmidlidl
 |-  ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j e. ( LIdeal ` R ) )
8 6 7 sylancom
 |-  ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> j e. ( LIdeal ` R ) )
9 eqid
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
10 9 3 lidl0cl
 |-  ( ( R e. Ring /\ j e. ( LIdeal ` R ) ) -> .0. e. j )
11 6 8 10 syl2anc
 |-  ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> .0. e. j )
12 11 snssd
 |-  ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> { .0. } C_ j )
13 5 12 eqsstrd
 |-  ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> i C_ j )
14 13 ralrimiva
 |-  ( ( R e. Ring /\ i = { .0. } ) -> A. j e. ( PrmIdeal ` R ) i C_ j )
15 rabid2
 |-  ( ( PrmIdeal ` R ) = { j e. ( PrmIdeal ` R ) | i C_ j } <-> A. j e. ( PrmIdeal ` R ) i C_ j )
16 14 15 sylibr
 |-  ( ( R e. Ring /\ i = { .0. } ) -> ( PrmIdeal ` R ) = { j e. ( PrmIdeal ` R ) | i C_ j } )
17 2 16 eqtr2id
 |-  ( ( R e. Ring /\ i = { .0. } ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = P )
18 9 3 lidl0
 |-  ( R e. Ring -> { .0. } e. ( LIdeal ` R ) )
19 2 fvexi
 |-  P e. _V
20 19 a1i
 |-  ( R e. Ring -> P e. _V )
21 4 17 18 20 fvmptd
 |-  ( R e. Ring -> ( V ` { .0. } ) = P )