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 No typesetting found for |- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |-
zarcls1.1 B = Base R
Assertion zarcls1 R CRing I LIdeal R V I = I = B

Proof

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