Theorem zarcls0

Description: The closure of the identity ideal in the Zariski topology. 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 |-
	zarcls0.1	No typesetting found for |- P = ( PrmIdeal ` R ) with typecode |-
	zarcls0.2	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	zarcls0	$$⊢R\in \mathrm{Ring}\to V\left(\left\{\underset{\dot{}}{0}\right\}\right)=P$$

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		zarcls0.1	Could not format P = ( PrmIdeal ` R ) : No typesetting found for |- P = ( PrmIdeal ` R ) with typecode |-
3		zarcls0.2	$$⊢\underset{\dot{}}{0}=0_R$$
4	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 |-
5		simplr	Could not format ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> i = { .0. } ) : No typesetting found for |- ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> i = { .0. } ) with typecode |-
6		simpll	Could not format ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> R e. Ring ) with typecode |-
7		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 |-
8	6 7	sylancom	Could not format ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> j e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> j e. ( LIdeal ` R ) ) with typecode |-
9		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
10	9 3	lidl0cl	$$⊢\left(R\in \mathrm{Ring}\wedge j\in \mathrm{LIdeal}\left(R\right)\right)\to \underset{\dot{}}{0}\in j$$
11	6 8 10	syl2anc	Could not format ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> .0. e. j ) : No typesetting found for |- ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> .0. e. j ) with typecode |-
12	11	snssd	Could not format ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> { .0. } C_ j ) : No typesetting found for |- ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> { .0. } C_ j ) with typecode |-
13	5 12	eqsstrd	Could not format ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> i C_ j ) : No typesetting found for |- ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> i C_ j ) with typecode |-
14	13	ralrimiva	Could not format ( ( R e. Ring /\ i = { .0. } ) -> A. j e. ( PrmIdeal ` R ) i C_ j ) : No typesetting found for |- ( ( R e. Ring /\ i = { .0. } ) -> A. j e. ( PrmIdeal ` R ) i C_ j ) with typecode |-
15		rabid2	Could not format ( ( PrmIdeal ` R ) = { j e. ( PrmIdeal ` R ) | i C_ j } <-> A. j e. ( PrmIdeal ` R ) i C_ j ) : No typesetting found for |- ( ( PrmIdeal ` R ) = { j e. ( PrmIdeal ` R ) | i C_ j } <-> A. j e. ( PrmIdeal ` R ) i C_ j ) with typecode |-
16	14 15	sylibr	Could not format ( ( R e. Ring /\ i = { .0. } ) -> ( PrmIdeal ` R ) = { j e. ( PrmIdeal ` R ) | i C_ j } ) : No typesetting found for |- ( ( R e. Ring /\ i = { .0. } ) -> ( PrmIdeal ` R ) = { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |-
17	2 16	eqtr2id	Could not format ( ( R e. Ring /\ i = { .0. } ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = P ) : No typesetting found for |- ( ( R e. Ring /\ i = { .0. } ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = P ) with typecode |-
18	9 3	lidl0	$$⊢R\in \mathrm{Ring}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(R\right)$$
19	2	fvexi	$$⊢P\in \mathrm{V}$$
20	19	a1i	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{V}$$
21	4 17 18 20	fvmptd	$$⊢R\in \mathrm{Ring}\to V\left(\left\{\underset{\dot{}}{0}\right\}\right)=P$$