rspectopn

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

	Ref	Expression
Hypotheses	rspecbas.1	No typesetting found for \|- S = ( Spec ` R ) with typecode \|-
	rspectopn.1	$⊢ I = LIdeal (R)$
	rspectopn.2	No typesetting found for \|- P = ( PrmIdeal ` R ) with typecode \|-
	rspectopn.3	$⊢ J = ran (i \in I ⟼ \{j \in P \| \neg i \subseteq j\})$
Assertion	rspectopn	$⊢ R \in Ring \to J = TopOpen (S)$

Proof

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

Metamath Proof Explorer

Theorem rspectopn

Proof