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	No typesetting found for |- S = ( Spec ` R ) with typecode |-
	zartop.2	$$⊢J=\mathrm{TopOpen}\left(S\right)$$
	zarmxt1.1	No typesetting found for |- M = ( MaxIdeal ` R ) with typecode |-
	zarmxt1.2	$$⊢T=J{\upharpoonright }_{𝑡}M$$
Assertion	zarmxt1	$$⊢R\in \mathrm{CRing}\to T\in \mathrm{Fre}$$

Proof

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