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