Metamath Proof Explorer

Theorem zarmxt1

Description: The Zariski topology restricted to maximal ideals is T_1 . (Contributed by Thierry Arnoux, 16-Jun-2024)

Ref Expression
Hypotheses zartop.1 
|- S = ( Spec ` R )
zartop.2 
|- J = ( TopOpen ` S )
zarmxt1.1 
|- M = ( MaxIdeal ` R )
zarmxt1.2 
|- T = ( J |`t M )
Assertion zarmxt1 
|- ( R e. CRing -> T e. Fre )

Proof

Step Hyp Ref Expression
1 zartop.1 
 |-  S = ( Spec ` R )
2 zartop.2 
 |-  J = ( TopOpen ` S )
3 zarmxt1.1 
 |-  M = ( MaxIdeal ` R )
4 zarmxt1.2 
 |-  T = ( J |`t M )
5 1 2 zartop 
 |-  ( R e. CRing -> J e. Top )
6 3 fvexi 
 |-  M e. _V
7 resttop 
 |-  ( ( J e. Top /\ M e. _V ) -> ( J |`t M ) e. Top )
8 4 7 eqeltrid 
 |-  ( ( J e. Top /\ M e. _V ) -> T e. Top )
9 5 6 8 sylancl 
 |-  ( R e. CRing -> T e. Top )
10 eqid 
 |-  ( LSSum ` ( mulGrp ` R ) ) = ( LSSum ` ( mulGrp ` R ) )
11 10 mxidlprm 
 |-  ( ( R e. CRing /\ m e. ( MaxIdeal ` R ) ) -> m e. ( PrmIdeal ` R ) )
12 11 ex 
 |-  ( R e. CRing -> ( m e. ( MaxIdeal ` R ) -> m e. ( PrmIdeal ` R ) ) )
13 12 ssrdv 
 |-  ( R e. CRing -> ( MaxIdeal ` R ) C_ ( PrmIdeal ` R ) )
14 13 adantr 
 |-  ( ( R e. CRing /\ m e. U. T ) -> ( MaxIdeal ` R ) C_ ( PrmIdeal ` R ) )
15 eqid 
 |-  ( PrmIdeal ` R ) = ( PrmIdeal ` R )
16 14 3 15 3sstr4g 
 |-  ( ( R e. CRing /\ m e. U. T ) -> M C_ ( PrmIdeal ` R ) )
17 sseq2 
 |-  ( j = l -> ( i C_ j <-> i C_ l ) )
18 17 cbvrabv 
 |-  { j e. ( PrmIdeal ` R ) | i C_ j } = { l e. ( PrmIdeal ` R ) | i C_ l }
19 sseq1 
 |-  ( i = k -> ( i C_ l <-> k C_ l ) )
20 19 rabbidv 
 |-  ( i = k -> { l e. ( PrmIdeal ` R ) | i C_ l } = { l e. ( PrmIdeal ` R ) | k C_ l } )
21 18 20 eqtrid 
 |-  ( i = k -> { j e. ( PrmIdeal ` R ) | i C_ j } = { l e. ( PrmIdeal ` R ) | k C_ l } )
22 21 cbvmptv 
 |-  ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) = ( k e. ( LIdeal ` R ) |-> { l e. ( PrmIdeal ` R ) | k C_ l } )
23 1 2 15 22 zartopn 
 |-  ( R e. CRing -> ( J e. ( TopOn ` ( PrmIdeal ` R ) ) /\ ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) = ( Clsd ` J ) ) )
24 23 adantr 
 |-  ( ( R e. CRing /\ m e. U. T ) -> ( J e. ( TopOn ` ( PrmIdeal ` R ) ) /\ ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) = ( Clsd ` J ) ) )
25 24 simpld 
 |-  ( ( R e. CRing /\ m e. U. T ) -> J e. ( TopOn ` ( PrmIdeal ` R ) ) )
26 toponuni 
 |-  ( J e. ( TopOn ` ( PrmIdeal ` R ) ) -> ( PrmIdeal ` R ) = U. J )
27 25 26 syl 
 |-  ( ( R e. CRing /\ m e. U. T ) -> ( PrmIdeal ` R ) = U. J )
28 16 27 sseqtrd 
 |-  ( ( R e. CRing /\ m e. U. T ) -> M C_ U. J )
29 simpl 
 |-  ( ( R e. CRing /\ m e. U. T ) -> R e. CRing )
30 29 crngringd 
 |-  ( ( R e. CRing /\ m e. U. T ) -> R e. Ring )
31 simpr 
 |-  ( ( R e. CRing /\ m e. U. T ) -> m e. U. T )
32 4 unieqi 
 |-  U. T = U. ( J |`t M )
33 31 32 eleqtrdi 
 |-  ( ( R e. CRing /\ m e. U. T ) -> m e. U. ( J |`t M ) )
34 5 adantr 
 |-  ( ( R e. CRing /\ m e. U. T ) -> J e. Top )
35 eqid 
 |-  U. J = U. J
36 35 restuni 
 |-  ( ( J e. Top /\ M C_ U. J ) -> M = U. ( J |`t M ) )
37 34 28 36 syl2anc 
 |-  ( ( R e. CRing /\ m e. U. T ) -> M = U. ( J |`t M ) )
38 33 37 eleqtrrd 
 |-  ( ( R e. CRing /\ m e. U. T ) -> m e. M )
39 38 3 eleqtrdi 
 |-  ( ( R e. CRing /\ m e. U. T ) -> m e. ( MaxIdeal ` R ) )
40 eqid 
 |-  ( Base ` R ) = ( Base ` R )
41 40 mxidlidl 
 |-  ( ( R e. Ring /\ m e. ( MaxIdeal ` R ) ) -> m e. ( LIdeal ` R ) )
42 30 39 41 syl2anc 
 |-  ( ( R e. CRing /\ m e. U. T ) -> m e. ( LIdeal ` R ) )
43 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
44 22 43 zarclssn 
 |-  ( ( R e. CRing /\ m e. ( LIdeal ` R ) ) -> ( { m } = ( ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ` m ) <-> m e. ( MaxIdeal ` R ) ) )
45 44 biimpar 
 |-  ( ( ( R e. CRing /\ m e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) -> { m } = ( ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ` m ) )
46 29 42 39 45 syl21anc 
 |-  ( ( R e. CRing /\ m e. U. T ) -> { m } = ( ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ` m ) )
47 22 funmpt2 
 |-  Fun ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
48 fvex 
 |-  ( PrmIdeal ` R ) e. _V
49 48 rabex 
 |-  { l e. ( PrmIdeal ` R ) | k C_ l } e. _V
50 49 22 dmmpti 
 |-  dom ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) = ( LIdeal ` R )
51 42 50 eleqtrrdi 
 |-  ( ( R e. CRing /\ m e. U. T ) -> m e. dom ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) )
52 fvelrn 
 |-  ( ( Fun ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) /\ m e. dom ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ) -> ( ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ` m ) e. ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) )
53 47 51 52 sylancr 
 |-  ( ( R e. CRing /\ m e. U. T ) -> ( ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ` m ) e. ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) )
54 46 53 eqeltrd 
 |-  ( ( R e. CRing /\ m e. U. T ) -> { m } e. ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) )
55 24 simprd 
 |-  ( ( R e. CRing /\ m e. U. T ) -> ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) = ( Clsd ` J ) )
56 54 55 eleqtrd 
 |-  ( ( R e. CRing /\ m e. U. T ) -> { m } e. ( Clsd ` J ) )
57 38 snssd 
 |-  ( ( R e. CRing /\ m e. U. T ) -> { m } C_ M )
58 35 restcldi 
 |-  ( ( M C_ U. J /\ { m } e. ( Clsd ` J ) /\ { m } C_ M ) -> { m } e. ( Clsd ` ( J |`t M ) ) )
59 28 56 57 58 syl3anc 
 |-  ( ( R e. CRing /\ m e. U. T ) -> { m } e. ( Clsd ` ( J |`t M ) ) )
60 4 fveq2i 
 |-  ( Clsd ` T ) = ( Clsd ` ( J |`t M ) )
61 59 60 eleqtrrdi 
 |-  ( ( R e. CRing /\ m e. U. T ) -> { m } e. ( Clsd ` T ) )
62 61 ralrimiva 
 |-  ( R e. CRing -> A. m e. U. T { m } e. ( Clsd ` T ) )
63 eqid 
 |-  U. T = U. T
64 63 ist1 
 |-  ( T e. Fre <-> ( T e. Top /\ A. m e. U. T { m } e. ( Clsd ` T ) ) )
65 9 62 64 sylanbrc 
 |-  ( R e. CRing -> T e. Fre )