Metamath Proof Explorer

Theorem zarcls1

Description: The unit ideal B is the only ideal whose closure in the Zariski topology is the empty set. Stronger form of the 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 } )
zarcls1.1 
|- B = ( Base ` R )
Assertion zarcls1 
|- ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> ( ( V ` I ) = (/) <-> I = B ) )

Proof

Step Hyp Ref Expression
1 zarclsx.1 
 |-  V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
2 zarcls1.1 
 |-  B = ( Base ` R )
3 simplr 
 |-  ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ ( V ` I ) = (/) ) /\ I =/= B ) -> ( V ` I ) = (/) )
4 sseq2 
 |-  ( j = m -> ( I C_ j <-> I C_ m ) )
5 eqid 
 |-  ( LSSum ` ( mulGrp ` R ) ) = ( LSSum ` ( mulGrp ` R ) )
6 5 mxidlprm 
 |-  ( ( R e. CRing /\ m e. ( MaxIdeal ` R ) ) -> m e. ( PrmIdeal ` R ) )
7 6 ad5ant14 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> m e. ( PrmIdeal ` R ) )
8 simpr 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> I C_ m )
9 4 7 8 elrabd 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> m e. { j e. ( PrmIdeal ` R ) | I C_ j } )
10 1 a1i 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) )
11 sseq1 
 |-  ( i = I -> ( i C_ j <-> I C_ j ) )
12 11 rabbidv 
 |-  ( i = I -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | I C_ j } )
13 12 adantl 
 |-  ( ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) /\ i = I ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | I C_ j } )
14 simp-4r 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> I e. ( LIdeal ` R ) )
15 fvex 
 |-  ( PrmIdeal ` R ) e. _V
16 15 rabex 
 |-  { j e. ( PrmIdeal ` R ) | I C_ j } e. _V
17 16 a1i 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> { j e. ( PrmIdeal ` R ) | I C_ j } e. _V )
18 10 13 14 17 fvmptd 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> ( V ` I ) = { j e. ( PrmIdeal ` R ) | I C_ j } )
19 9 18 eleqtrrd 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> m e. ( V ` I ) )
20 ne0i 
 |-  ( m e. ( V ` I ) -> ( V ` I ) =/= (/) )
21 19 20 syl 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> ( V ` I ) =/= (/) )
22 crngring 
 |-  ( R e. CRing -> R e. Ring )
23 2 ssmxidl 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m )
24 23 3expa 
 |-  ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m )
25 22 24 sylanl1 
 |-  ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m )
26 21 25 r19.29a 
 |-  ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) -> ( V ` I ) =/= (/) )
27 26 adantlr 
 |-  ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ ( V ` I ) = (/) ) /\ I =/= B ) -> ( V ` I ) =/= (/) )
28 27 neneqd 
 |-  ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ ( V ` I ) = (/) ) /\ I =/= B ) -> -. ( V ` I ) = (/) )
29 3 28 pm2.65da 
 |-  ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ ( V ` I ) = (/) ) -> -. I =/= B )
30 nne 
 |-  ( -. I =/= B <-> I = B )
31 29 30 sylib 
 |-  ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ ( V ` I ) = (/) ) -> I = B )
32 fveq2 
 |-  ( I = B -> ( V ` I ) = ( V ` B ) )
33 32 adantl 
 |-  ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I = B ) -> ( V ` I ) = ( V ` B ) )
34 1 a1i 
 |-  ( R e. Ring -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) )
35 sseq1 
 |-  ( i = B -> ( i C_ j <-> B C_ j ) )
36 35 adantl 
 |-  ( ( R e. Ring /\ i = B ) -> ( i C_ j <-> B C_ j ) )
37 36 rabbidv 
 |-  ( ( R e. Ring /\ i = B ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | B C_ j } )
38 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
39 38 2 lidl1 
 |-  ( R e. Ring -> B e. ( LIdeal ` R ) )
40 15 rabex 
 |-  { j e. ( PrmIdeal ` R ) | B C_ j } e. _V
41 40 a1i 
 |-  ( R e. Ring -> { j e. ( PrmIdeal ` R ) | B C_ j } e. _V )
42 34 37 39 41 fvmptd 
 |-  ( R e. Ring -> ( V ` B ) = { j e. ( PrmIdeal ` R ) | B C_ j } )
43 prmidlidl 
 |-  ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j e. ( LIdeal ` R ) )
44 2 38 lidlss 
 |-  ( j e. ( LIdeal ` R ) -> j C_ B )
45 43 44 syl 
 |-  ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j C_ B )
46 45 adantr 
 |-  ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> j C_ B )
47 simpr 
 |-  ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> B C_ j )
48 46 47 eqssd 
 |-  ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> j = B )
49 eqid 
 |-  ( .r ` R ) = ( .r ` R )
50 2 49 prmidlnr 
 |-  ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j =/= B )
51 50 adantr 
 |-  ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> j =/= B )
52 51 neneqd 
 |-  ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> -. j = B )
53 48 52 pm2.65da 
 |-  ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> -. B C_ j )
54 53 ralrimiva 
 |-  ( R e. Ring -> A. j e. ( PrmIdeal ` R ) -. B C_ j )
55 rabeq0 
 |-  ( { j e. ( PrmIdeal ` R ) | B C_ j } = (/) <-> A. j e. ( PrmIdeal ` R ) -. B C_ j )
56 54 55 sylibr 
 |-  ( R e. Ring -> { j e. ( PrmIdeal ` R ) | B C_ j } = (/) )
57 42 56 eqtrd 
 |-  ( R e. Ring -> ( V ` B ) = (/) )
58 22 57 syl 
 |-  ( R e. CRing -> ( V ` B ) = (/) )
59 58 ad2antrr 
 |-  ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I = B ) -> ( V ` B ) = (/) )
60 33 59 eqtrd 
 |-  ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I = B ) -> ( V ` I ) = (/) )
61 31 60 impbida 
 |-  ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> ( ( V ` I ) = (/) <-> I = B ) )