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

Metamath Proof Explorer

Theorem zarmxt1

Proof