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	|- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
	zarcls0.1	|- P = ( PrmIdeal ` R )
	zarcls0.2	|- .0. = ( 0g ` R )
Assertion	zarcls0	|- ( R e. Ring -> ( V ` { .0. } ) = P )

Proof

Step	Hyp	Ref	Expression
1		zarclsx.1	|- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
2		zarcls0.1	|- P = ( PrmIdeal ` R )
3		zarcls0.2	|- .0. = ( 0g ` R )
4	1	a1i	|- ( R e. Ring -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) )
5		simplr	|- ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> i = { .0. } )
6		simpll	|- ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> R e. Ring )
7		prmidlidl	|- ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j e. ( LIdeal ` R ) )
8	6 7	sylancom	|- ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> j e. ( LIdeal ` R ) )
9		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
10	9 3	lidl0cl	|- ( ( R e. Ring /\ j e. ( LIdeal ` R ) ) -> .0. e. j )
11	6 8 10	syl2anc	|- ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> .0. e. j )
12	11	snssd	|- ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> { .0. } C_ j )
13	5 12	eqsstrd	|- ( ( ( R e. Ring /\ i = { .0. } ) /\ j e. ( PrmIdeal ` R ) ) -> i C_ j )
14	13	ralrimiva	|- ( ( R e. Ring /\ i = { .0. } ) -> A. j e. ( PrmIdeal ` R ) i C_ j )
15		rabid2	|- ( ( PrmIdeal ` R ) = { j e. ( PrmIdeal ` R ) | i C_ j } <-> A. j e. ( PrmIdeal ` R ) i C_ j )
16	14 15	sylibr	|- ( ( R e. Ring /\ i = { .0. } ) -> ( PrmIdeal ` R ) = { j e. ( PrmIdeal ` R ) | i C_ j } )
17	2 16	syl5req	|- ( ( R e. Ring /\ i = { .0. } ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = P )
18	9 3	lidl0	|- ( R e. Ring -> { .0. } e. ( LIdeal ` R ) )
19	2	fvexi	|- P e. _V
20	19	a1i	|- ( R e. Ring -> P e. _V )
21	4 17 18 20	fvmptd	|- ( R e. Ring -> ( V ` { .0. } ) = P )