Metamath Proof Explorer

Theorem zarclssn

Description: The closed points of Zariski topology are the maximal ideals. (Contributed by Thierry Arnoux, 16-Jun-2024)

Ref Expression
Hypotheses zarclsx.1 
|- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
zarclssn.1 
|- B = ( LIdeal ` R )
Assertion zarclssn 
|- ( ( R e. CRing /\ M e. B ) -> ( { M } = ( V ` M ) <-> M e. ( MaxIdeal ` R ) ) )

Proof

Step Hyp Ref Expression
1 zarclsx.1 
 |-  V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
2 zarclssn.1 
 |-  B = ( LIdeal ` R )
3 crngring 
 |-  ( R e. CRing -> R e. Ring )
4 3 ad2antrr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> R e. Ring )
5 simplr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> M e. B )
6 5 2 eleqtrdi 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> M e. ( LIdeal ` R ) )
7 simpr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> { M } = ( V ` M ) )
8 snnzg 
 |-  ( M e. B -> { M } =/= (/) )
9 5 8 syl 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> { M } =/= (/) )
10 7 9 eqnetrrd 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> ( V ` M ) =/= (/) )
11 simpll 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> R e. CRing )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 1 12 zarcls1 
 |-  ( ( R e. CRing /\ M e. ( LIdeal ` R ) ) -> ( ( V ` M ) = (/) <-> M = ( Base ` R ) ) )
14 13 necon3bid 
 |-  ( ( R e. CRing /\ M e. ( LIdeal ` R ) ) -> ( ( V ` M ) =/= (/) <-> M =/= ( Base ` R ) ) )
15 11 6 14 syl2anc 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> ( ( V ` M ) =/= (/) <-> M =/= ( Base ` R ) ) )
16 10 15 mpbid 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> M =/= ( Base ` R ) )
17 simpr 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> j C_ m )
18 11 ad5antr 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> R e. CRing )
19 simplr 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> m e. ( MaxIdeal ` R ) )
20 eqid 
 |-  ( LSSum ` ( mulGrp ` R ) ) = ( LSSum ` ( mulGrp ` R ) )
21 20 mxidlprm 
 |-  ( ( R e. CRing /\ m e. ( MaxIdeal ` R ) ) -> m e. ( PrmIdeal ` R ) )
22 18 19 21 syl2anc 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> m e. ( PrmIdeal ` R ) )
23 simp-4r 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> M C_ j )
24 23 17 sstrd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> M C_ m )
25 1 a1i 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) )
26 sseq1 
 |-  ( i = M -> ( i C_ j <-> M C_ j ) )
27 26 rabbidv 
 |-  ( i = M -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | M C_ j } )
28 27 adantl 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ i = M ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | M C_ j } )
29 fvex 
 |-  ( PrmIdeal ` R ) e. _V
30 29 rabex 
 |-  { j e. ( PrmIdeal ` R ) | M C_ j } e. _V
31 30 a1i 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> { j e. ( PrmIdeal ` R ) | M C_ j } e. _V )
32 25 28 6 31 fvmptd 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> ( V ` M ) = { j e. ( PrmIdeal ` R ) | M C_ j } )
33 7 32 eqtr2d 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> { j e. ( PrmIdeal ` R ) | M C_ j } = { M } )
34 rabeqsn 
 |-  ( { j e. ( PrmIdeal ` R ) | M C_ j } = { M } <-> A. j ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) )
35 33 34 sylib 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> A. j ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) )
36 35 ad5antr 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> A. j ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) )
37 vex 
 |-  m e. _V
38 eleq1w 
 |-  ( j = m -> ( j e. ( PrmIdeal ` R ) <-> m e. ( PrmIdeal ` R ) ) )
39 sseq2 
 |-  ( j = m -> ( M C_ j <-> M C_ m ) )
40 38 39 anbi12d 
 |-  ( j = m -> ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> ( m e. ( PrmIdeal ` R ) /\ M C_ m ) ) )
41 eqeq1 
 |-  ( j = m -> ( j = M <-> m = M ) )
42 40 41 bibi12d 
 |-  ( j = m -> ( ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) <-> ( ( m e. ( PrmIdeal ` R ) /\ M C_ m ) <-> m = M ) ) )
43 37 42 spcv 
 |-  ( A. j ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) -> ( ( m e. ( PrmIdeal ` R ) /\ M C_ m ) <-> m = M ) )
44 36 43 syl 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> ( ( m e. ( PrmIdeal ` R ) /\ M C_ m ) <-> m = M ) )
45 22 24 44 mpbi2and 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> m = M )
46 17 45 sseqtrd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> j C_ M )
47 46 23 eqssd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> j = M )
48 3 ad5antr 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) -> R e. Ring )
49 simpllr 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) -> j e. ( LIdeal ` R ) )
50 simpr 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) -> -. j = ( Base ` R ) )
51 50 neqned 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) -> j =/= ( Base ` R ) )
52 12 ssmxidl 
 |-  ( ( R e. Ring /\ j e. ( LIdeal ` R ) /\ j =/= ( Base ` R ) ) -> E. m e. ( MaxIdeal ` R ) j C_ m )
53 48 49 51 52 syl3anc 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) -> E. m e. ( MaxIdeal ` R ) j C_ m )
54 47 53 r19.29a 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) -> j = M )
55 54 ex 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) -> ( -. j = ( Base ` R ) -> j = M ) )
56 55 orrd 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) -> ( j = ( Base ` R ) \/ j = M ) )
57 56 orcomd 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) -> ( j = M \/ j = ( Base ` R ) ) )
58 57 ex 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) -> ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) )
59 58 ralrimiva 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) )
60 6 16 59 3jca 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> ( M e. ( LIdeal ` R ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) )
61 12 ismxidl 
 |-  ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) )
62 61 biimpar 
 |-  ( ( R e. Ring /\ ( M e. ( LIdeal ` R ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) -> M e. ( MaxIdeal ` R ) )
63 4 60 62 syl2anc 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> M e. ( MaxIdeal ` R ) )
64 1 a1i 
 |-  ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) )
65 27 adantl 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ i = M ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | M C_ j } )
66 12 mxidlidl 
 |-  ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) )
67 3 66 sylan 
 |-  ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) )
68 30 a1i 
 |-  ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | M C_ j } e. _V )
69 64 65 67 68 fvmptd 
 |-  ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> ( V ` M ) = { j e. ( PrmIdeal ` R ) | M C_ j } )
70 3 ad2antrr 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> R e. Ring )
71 simplr 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> M e. ( MaxIdeal ` R ) )
72 simprl 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> j e. ( PrmIdeal ` R ) )
73 prmidlidl 
 |-  ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j e. ( LIdeal ` R ) )
74 70 72 73 syl2anc 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> j e. ( LIdeal ` R ) )
75 simprr 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> M C_ j )
76 74 75 jca 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> ( j e. ( LIdeal ` R ) /\ M C_ j ) )
77 12 mxidlmax 
 |-  ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( LIdeal ` R ) /\ M C_ j ) ) -> ( j = M \/ j = ( Base ` R ) ) )
78 70 71 76 77 syl21anc 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> ( j = M \/ j = ( Base ` R ) ) )
79 eqid 
 |-  ( .r ` R ) = ( .r ` R )
80 12 79 prmidlnr 
 |-  ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j =/= ( Base ` R ) )
81 70 72 80 syl2anc 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> j =/= ( Base ` R ) )
82 81 neneqd 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> -. j = ( Base ` R ) )
83 78 82 olcnd 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> j = M )
84 simpr 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> j = M )
85 20 mxidlprm 
 |-  ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M e. ( PrmIdeal ` R ) )
86 85 adantr 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> M e. ( PrmIdeal ` R ) )
87 84 86 eqeltrd 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> j e. ( PrmIdeal ` R ) )
88 ssidd 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> j C_ j )
89 84 88 eqsstrrd 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> M C_ j )
90 87 89 jca 
 |-  ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> ( j e. ( PrmIdeal ` R ) /\ M C_ j ) )
91 83 90 impbida 
 |-  ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) )
92 91 alrimiv 
 |-  ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> A. j ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) )
93 92 34 sylibr 
 |-  ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | M C_ j } = { M } )
94 69 93 eqtr2d 
 |-  ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> { M } = ( V ` M ) )
95 94 adantlr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. ( MaxIdeal ` R ) ) -> { M } = ( V ` M ) )
96 63 95 impbida 
 |-  ( ( R e. CRing /\ M e. B ) -> ( { M } = ( V ` M ) <-> M e. ( MaxIdeal ` R ) ) )