Theorem zarcls1

Description: The unit ideal B is the only ideal whose closure in the Zariski topology is the empty set. Stronger form of the Proposition 1.1.2(i) of EGA p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024)

	Ref	Expression
Hypotheses	zarclsx.1	No typesetting found for |- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |-
	zarcls1.1	$$⊢B={\mathrm{Base}}_R$$
Assertion	zarcls1	$$⊢\left(R\in \mathrm{CRing}\wedge I\in \mathrm{LIdeal}\left(R\right)\right)\to \left(V\left(I\right)=\varnothing \leftrightarrow I=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		zarclsx.1	Could not format V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) : No typesetting found for |- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |-
2		zarcls1.1	$$⊢B={\mathrm{Base}}_R$$
3		simplr	$$⊢\left(\left(\left(R\in \mathrm{CRing}\wedge I\in \mathrm{LIdeal}\left(R\right)\right)\wedge V\left(I\right)=\varnothing \right)\wedge I\ne B\right)\to V\left(I\right)=\varnothing$$
4		sseq2	$$⊢j=m\to \left(I\subseteq j\leftrightarrow I\subseteq m\right)$$
5		eqid	$$⊢\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)=\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)$$
6	5	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 |-
7	6	ad5ant14	Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> m e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> m e. ( PrmIdeal ` R ) ) with typecode |-
8		simpr	Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> I C_ m ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> I C_ m ) with typecode |-
9	4 7 8	elrabd	Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> m e. { j e. ( PrmIdeal ` R ) | I C_ j } ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> m e. { j e. ( PrmIdeal ` R ) | I C_ j } ) with typecode |-
10	1	a1i	Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ) with typecode |-
11		sseq1	$$⊢i=I\to \left(i\subseteq j\leftrightarrow I\subseteq j\right)$$
12	11	rabbidv	Could not format ( i = I -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | I C_ j } ) : No typesetting found for |- ( i = I -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | I C_ j } ) with typecode |-
13	12	adantl	Could not format ( ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) /\ i = I ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | I C_ j } ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) /\ i = I ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | I C_ j } ) with typecode |-
14		simp-4r	Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> I e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> I e. ( LIdeal ` R ) ) with typecode |-
15		fvex	Could not format ( PrmIdeal ` R ) e. _V : No typesetting found for |- ( PrmIdeal ` R ) e. _V with typecode |-
16	15	rabex	Could not format { j e. ( PrmIdeal ` R ) | I C_ j } e. _V : No typesetting found for |- { j e. ( PrmIdeal ` R ) | I C_ j } e. _V with typecode |-
17	16	a1i	Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> { j e. ( PrmIdeal ` R ) | I C_ j } e. _V ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> { j e. ( PrmIdeal ` R ) | I C_ j } e. _V ) with typecode |-
18	10 13 14 17	fvmptd	Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> ( V ` I ) = { j e. ( PrmIdeal ` R ) | I C_ j } ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> ( V ` I ) = { j e. ( PrmIdeal ` R ) | I C_ j } ) with typecode |-
19	9 18	eleqtrrd	Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> m e. ( V ` I ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> m e. ( V ` I ) ) with typecode |-
20		ne0i	$$⊢m\in V\left(I\right)\to V\left(I\right)\ne \varnothing$$
21	19 20	syl	Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> ( V ` I ) =/= (/) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> ( V ` I ) =/= (/) ) with typecode |-
22		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
23	2	ssmxidl	Could not format ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m ) : No typesetting found for |- ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m ) with typecode |-
24	23	3expa	Could not format ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m ) : No typesetting found for |- ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m ) with typecode |-
25	22 24	sylanl1	Could not format ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m ) : No typesetting found for |- ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m ) with typecode |-
26	21 25	r19.29a	$$⊢\left(\left(R\in \mathrm{CRing}\wedge I\in \mathrm{LIdeal}\left(R\right)\right)\wedge I\ne B\right)\to V\left(I\right)\ne \varnothing$$
27	26	adantlr	$$⊢\left(\left(\left(R\in \mathrm{CRing}\wedge I\in \mathrm{LIdeal}\left(R\right)\right)\wedge V\left(I\right)=\varnothing \right)\wedge I\ne B\right)\to V\left(I\right)\ne \varnothing$$
28	27	neneqd	$$⊢\left(\left(\left(R\in \mathrm{CRing}\wedge I\in \mathrm{LIdeal}\left(R\right)\right)\wedge V\left(I\right)=\varnothing \right)\wedge I\ne B\right)\to \neg V\left(I\right)=\varnothing$$
29	3 28	pm2.65da	$$⊢\left(\left(R\in \mathrm{CRing}\wedge I\in \mathrm{LIdeal}\left(R\right)\right)\wedge V\left(I\right)=\varnothing \right)\to \neg I\ne B$$
30		nne	$$⊢\neg I\ne B\leftrightarrow I=B$$
31	29 30	sylib	$$⊢\left(\left(R\in \mathrm{CRing}\wedge I\in \mathrm{LIdeal}\left(R\right)\right)\wedge V\left(I\right)=\varnothing \right)\to I=B$$
32		fveq2	$$⊢I=B\to V\left(I\right)=V\left(B\right)$$
33	32	adantl	$$⊢\left(\left(R\in \mathrm{CRing}\wedge I\in \mathrm{LIdeal}\left(R\right)\right)\wedge I=B\right)\to V\left(I\right)=V\left(B\right)$$
34	1	a1i	Could not format ( R e. Ring -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ) : No typesetting found for |- ( R e. Ring -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ) with typecode |-
35		sseq1	$$⊢i=B\to \left(i\subseteq j\leftrightarrow B\subseteq j\right)$$
36	35	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge i=B\right)\to \left(i\subseteq j\leftrightarrow B\subseteq j\right)$$
37	36	rabbidv	Could not format ( ( R e. Ring /\ i = B ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | B C_ j } ) : No typesetting found for |- ( ( R e. Ring /\ i = B ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | B C_ j } ) with typecode |-
38		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
39	38 2	lidl1	$$⊢R\in \mathrm{Ring}\to B\in \mathrm{LIdeal}\left(R\right)$$
40	15	rabex	Could not format { j e. ( PrmIdeal ` R ) | B C_ j } e. _V : No typesetting found for |- { j e. ( PrmIdeal ` R ) | B C_ j } e. _V with typecode |-
41	40	a1i	Could not format ( R e. Ring -> { j e. ( PrmIdeal ` R ) | B C_ j } e. _V ) : No typesetting found for |- ( R e. Ring -> { j e. ( PrmIdeal ` R ) | B C_ j } e. _V ) with typecode |-
42	34 37 39 41	fvmptd	Could not format ( R e. Ring -> ( V ` B ) = { j e. ( PrmIdeal ` R ) | B C_ j } ) : No typesetting found for |- ( R e. Ring -> ( V ` B ) = { j e. ( PrmIdeal ` R ) | B C_ j } ) with typecode |-
43		prmidlidl	Could not format ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j e. ( LIdeal ` R ) ) with typecode |-
44	2 38	lidlss	$$⊢j\in \mathrm{LIdeal}\left(R\right)\to j\subseteq B$$
45	43 44	syl	Could not format ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j C_ B ) : No typesetting found for |- ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j C_ B ) with typecode |-
46	45	adantr	Could not format ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> j C_ B ) : No typesetting found for |- ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> j C_ B ) with typecode |-
47		simpr	Could not format ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> B C_ j ) : No typesetting found for |- ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> B C_ j ) with typecode |-
48	46 47	eqssd	Could not format ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> j = B ) : No typesetting found for |- ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> j = B ) with typecode |-
49		eqid	$$⊢{\cdot }_R={\cdot }_R$$
50	2 49	prmidlnr	Could not format ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j =/= B ) : No typesetting found for |- ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j =/= B ) with typecode |-
51	50	adantr	Could not format ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> j =/= B ) : No typesetting found for |- ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> j =/= B ) with typecode |-
52	51	neneqd	Could not format ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> -. j = B ) : No typesetting found for |- ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> -. j = B ) with typecode |-
53	48 52	pm2.65da	Could not format ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> -. B C_ j ) : No typesetting found for |- ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> -. B C_ j ) with typecode |-
54	53	ralrimiva	Could not format ( R e. Ring -> A. j e. ( PrmIdeal ` R ) -. B C_ j ) : No typesetting found for |- ( R e. Ring -> A. j e. ( PrmIdeal ` R ) -. B C_ j ) with typecode |-
55		rabeq0	Could not format ( { j e. ( PrmIdeal ` R ) | B C_ j } = (/) <-> A. j e. ( PrmIdeal ` R ) -. B C_ j ) : No typesetting found for |- ( { j e. ( PrmIdeal ` R ) | B C_ j } = (/) <-> A. j e. ( PrmIdeal ` R ) -. B C_ j ) with typecode |-
56	54 55	sylibr	Could not format ( R e. Ring -> { j e. ( PrmIdeal ` R ) | B C_ j } = (/) ) : No typesetting found for |- ( R e. Ring -> { j e. ( PrmIdeal ` R ) | B C_ j } = (/) ) with typecode |-
57	42 56	eqtrd	$$⊢R\in \mathrm{Ring}\to V\left(B\right)=\varnothing$$
58	22 57	syl	$$⊢R\in \mathrm{CRing}\to V\left(B\right)=\varnothing$$
59	58	ad2antrr	$$⊢\left(\left(R\in \mathrm{CRing}\wedge I\in \mathrm{LIdeal}\left(R\right)\right)\wedge I=B\right)\to V\left(B\right)=\varnothing$$
60	33 59	eqtrd	$$⊢\left(\left(R\in \mathrm{CRing}\wedge I\in \mathrm{LIdeal}\left(R\right)\right)\wedge I=B\right)\to V\left(I\right)=\varnothing$$
61	31 60	impbida	$$⊢\left(R\in \mathrm{CRing}\wedge I\in \mathrm{LIdeal}\left(R\right)\right)\to \left(V\left(I\right)=\varnothing \leftrightarrow I=B\right)$$