rspectopn

Description: The topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 4-Jun-2024)

	Ref	Expression
Hypotheses	rspecbas.1	\|- S = ( Spec ` R )
	rspectopn.1	\|- I = ( LIdeal ` R )
	rspectopn.2	\|- P = ( PrmIdeal ` R )
	rspectopn.3	\|- J = ran ( i e. I \|-> { j e. P \| -. i C_ j } )
Assertion	rspectopn	\|- ( R e. Ring -> J = ( TopOpen ` S ) )

Proof

Step	Hyp	Ref	Expression
1		rspecbas.1	\|- S = ( Spec ` R )
2		rspectopn.1	\|- I = ( LIdeal ` R )
3		rspectopn.2	\|- P = ( PrmIdeal ` R )
4		rspectopn.3	\|- J = ran ( i e. I \|-> { j e. P \| -. i C_ j } )
5		rspecval	\|- ( R e. Ring -> ( Spec ` R ) = ( ( IDLsrg ` R ) \|`s ( PrmIdeal ` R ) ) )
6	3	oveq2i	\|- ( ( IDLsrg ` R ) \|`s P ) = ( ( IDLsrg ` R ) \|`s ( PrmIdeal ` R ) )
7	5 1 6	3eqtr4g	\|- ( R e. Ring -> S = ( ( IDLsrg ` R ) \|`s P ) )
8	7	fveq2d	\|- ( R e. Ring -> ( TopOpen ` S ) = ( TopOpen ` ( ( IDLsrg ` R ) \|`s P ) ) )
9		eqid	\|- ( ( IDLsrg ` R ) \|`s P ) = ( ( IDLsrg ` R ) \|`s P )
10		eqid	\|- ( TopOpen ` ( IDLsrg ` R ) ) = ( TopOpen ` ( IDLsrg ` R ) )
11	9 10	resstopn	\|- ( ( TopOpen ` ( IDLsrg ` R ) ) \|`t P ) = ( TopOpen ` ( ( IDLsrg ` R ) \|`s P ) )
12	8 11	eqtr4di	\|- ( R e. Ring -> ( TopOpen ` S ) = ( ( TopOpen ` ( IDLsrg ` R ) ) \|`t P ) )
13		eqid	\|- ( IDLsrg ` R ) = ( IDLsrg ` R )
14		eqid	\|- ran ( i e. I \|-> { j e. I \| -. i C_ j } ) = ran ( i e. I \|-> { j e. I \| -. i C_ j } )
15	13 2 14	idlsrgtset	\|- ( R e. Ring -> ran ( i e. I \|-> { j e. I \| -. i C_ j } ) = ( TopSet ` ( IDLsrg ` R ) ) )
16	2	fvexi	\|- I e. _V
17	16	rabex	\|- { j e. I \| -. i C_ j } e. _V
18	17	a1i	\|- ( ( R e. Ring /\ i e. I ) -> { j e. I \| -. i C_ j } e. _V )
19		simp2	\|- ( ( ( R e. Ring /\ i e. I ) /\ j e. I /\ -. i C_ j ) -> j e. I )
20	13 2	idlsrgbas	\|- ( R e. Ring -> I = ( Base ` ( IDLsrg ` R ) ) )
21	20	adantr	\|- ( ( R e. Ring /\ i e. I ) -> I = ( Base ` ( IDLsrg ` R ) ) )
22	21	3ad2ant1	\|- ( ( ( R e. Ring /\ i e. I ) /\ j e. I /\ -. i C_ j ) -> I = ( Base ` ( IDLsrg ` R ) ) )
23	19 22	eleqtrd	\|- ( ( ( R e. Ring /\ i e. I ) /\ j e. I /\ -. i C_ j ) -> j e. ( Base ` ( IDLsrg ` R ) ) )
24	23	rabssdv	\|- ( ( R e. Ring /\ i e. I ) -> { j e. I \| -. i C_ j } C_ ( Base ` ( IDLsrg ` R ) ) )
25	18 24	elpwd	\|- ( ( R e. Ring /\ i e. I ) -> { j e. I \| -. i C_ j } e. ~P ( Base ` ( IDLsrg ` R ) ) )
26	25	ralrimiva	\|- ( R e. Ring -> A. i e. I { j e. I \| -. i C_ j } e. ~P ( Base ` ( IDLsrg ` R ) ) )
27		eqid	\|- ( i e. I \|-> { j e. I \| -. i C_ j } ) = ( i e. I \|-> { j e. I \| -. i C_ j } )
28	27	rnmptss	\|- ( A. i e. I { j e. I \| -. i C_ j } e. ~P ( Base ` ( IDLsrg ` R ) ) -> ran ( i e. I \|-> { j e. I \| -. i C_ j } ) C_ ~P ( Base ` ( IDLsrg ` R ) ) )
29	26 28	syl	\|- ( R e. Ring -> ran ( i e. I \|-> { j e. I \| -. i C_ j } ) C_ ~P ( Base ` ( IDLsrg ` R ) ) )
30	15 29	eqsstrrd	\|- ( R e. Ring -> ( TopSet ` ( IDLsrg ` R ) ) C_ ~P ( Base ` ( IDLsrg ` R ) ) )
31		eqid	\|- ( Base ` ( IDLsrg ` R ) ) = ( Base ` ( IDLsrg ` R ) )
32		eqid	\|- ( TopSet ` ( IDLsrg ` R ) ) = ( TopSet ` ( IDLsrg ` R ) )
33	31 32	topnid	\|- ( ( TopSet ` ( IDLsrg ` R ) ) C_ ~P ( Base ` ( IDLsrg ` R ) ) -> ( TopSet ` ( IDLsrg ` R ) ) = ( TopOpen ` ( IDLsrg ` R ) ) )
34	30 33	syl	\|- ( R e. Ring -> ( TopSet ` ( IDLsrg ` R ) ) = ( TopOpen ` ( IDLsrg ` R ) ) )
35	15 34	eqtrd	\|- ( R e. Ring -> ran ( i e. I \|-> { j e. I \| -. i C_ j } ) = ( TopOpen ` ( IDLsrg ` R ) ) )
36	35	oveq1d	\|- ( R e. Ring -> ( ran ( i e. I \|-> { j e. I \| -. i C_ j } ) \|`t P ) = ( ( TopOpen ` ( IDLsrg ` R ) ) \|`t P ) )
37	16	mptex	\|- ( i e. I \|-> { j e. I \| -. i C_ j } ) e. _V
38	37	rnex	\|- ran ( i e. I \|-> { j e. I \| -. i C_ j } ) e. _V
39	3	fvexi	\|- P e. _V
40		elrest	\|- ( ( ran ( i e. I \|-> { j e. I \| -. i C_ j } ) e. _V /\ P e. _V ) -> ( x e. ( ran ( i e. I \|-> { j e. I \| -. i C_ j } ) \|`t P ) <-> E. y e. ran ( i e. I \|-> { j e. I \| -. i C_ j } ) x = ( y i^i P ) ) )
41	38 39 40	mp2an	\|- ( x e. ( ran ( i e. I \|-> { j e. I \| -. i C_ j } ) \|`t P ) <-> E. y e. ran ( i e. I \|-> { j e. I \| -. i C_ j } ) x = ( y i^i P ) )
42	17	rgenw	\|- A. i e. I { j e. I \| -. i C_ j } e. _V
43		ineq1	\|- ( y = { j e. I \| -. i C_ j } -> ( y i^i P ) = ( { j e. I \| -. i C_ j } i^i P ) )
44	43	eqeq2d	\|- ( y = { j e. I \| -. i C_ j } -> ( x = ( y i^i P ) <-> x = ( { j e. I \| -. i C_ j } i^i P ) ) )
45	27 44	rexrnmptw	\|- ( A. i e. I { j e. I \| -. i C_ j } e. _V -> ( E. y e. ran ( i e. I \|-> { j e. I \| -. i C_ j } ) x = ( y i^i P ) <-> E. i e. I x = ( { j e. I \| -. i C_ j } i^i P ) ) )
46	42 45	ax-mp	\|- ( E. y e. ran ( i e. I \|-> { j e. I \| -. i C_ j } ) x = ( y i^i P ) <-> E. i e. I x = ( { j e. I \| -. i C_ j } i^i P ) )
47		inrab2	\|- ( { j e. I \| -. i C_ j } i^i P ) = { j e. ( I i^i P ) \| -. i C_ j }
48		prmidlssidl	\|- ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) )
49	48 3 2	3sstr4g	\|- ( R e. Ring -> P C_ I )
50		sseqin2	\|- ( P C_ I <-> ( I i^i P ) = P )
51	49 50	sylib	\|- ( R e. Ring -> ( I i^i P ) = P )
52	51	rabeqdv	\|- ( R e. Ring -> { j e. ( I i^i P ) \| -. i C_ j } = { j e. P \| -. i C_ j } )
53	47 52	eqtrid	\|- ( R e. Ring -> ( { j e. I \| -. i C_ j } i^i P ) = { j e. P \| -. i C_ j } )
54	53	eqeq2d	\|- ( R e. Ring -> ( x = ( { j e. I \| -. i C_ j } i^i P ) <-> x = { j e. P \| -. i C_ j } ) )
55	54	rexbidv	\|- ( R e. Ring -> ( E. i e. I x = ( { j e. I \| -. i C_ j } i^i P ) <-> E. i e. I x = { j e. P \| -. i C_ j } ) )
56	46 55	bitrid	\|- ( R e. Ring -> ( E. y e. ran ( i e. I \|-> { j e. I \| -. i C_ j } ) x = ( y i^i P ) <-> E. i e. I x = { j e. P \| -. i C_ j } ) )
57	41 56	bitrid	\|- ( R e. Ring -> ( x e. ( ran ( i e. I \|-> { j e. I \| -. i C_ j } ) \|`t P ) <-> E. i e. I x = { j e. P \| -. i C_ j } ) )
58	4	eleq2i	\|- ( x e. J <-> x e. ran ( i e. I \|-> { j e. P \| -. i C_ j } ) )
59		eqid	\|- ( i e. I \|-> { j e. P \| -. i C_ j } ) = ( i e. I \|-> { j e. P \| -. i C_ j } )
60	39	rabex	\|- { j e. P \| -. i C_ j } e. _V
61	59 60	elrnmpti	\|- ( x e. ran ( i e. I \|-> { j e. P \| -. i C_ j } ) <-> E. i e. I x = { j e. P \| -. i C_ j } )
62	58 61	bitri	\|- ( x e. J <-> E. i e. I x = { j e. P \| -. i C_ j } )
63	57 62	bitr4di	\|- ( R e. Ring -> ( x e. ( ran ( i e. I \|-> { j e. I \| -. i C_ j } ) \|`t P ) <-> x e. J ) )
64	63	eqrdv	\|- ( R e. Ring -> ( ran ( i e. I \|-> { j e. I \| -. i C_ j } ) \|`t P ) = J )
65	12 36 64	3eqtr2rd	\|- ( R e. Ring -> J = ( TopOpen ` S ) )

Metamath Proof Explorer

Theorem rspectopn

Proof