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 \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	$⊢ S = Spec (R)$
2		rspectopn.1	$⊢ I = LIdeal (R)$
3		rspectopn.2	$⊢ P = PrmIdeal (R)$
4		rspectopn.3	$⊢ J = ran (i \in I ⟼ \{j \in P \| \neg i \subseteq j\})$
5		rspecval	$⊢ R \in Ring \to Spec (R) = IDLsrg (R) ↾_{𝑠} PrmIdeal (R)$
6	3	oveq2i	$⊢ IDLsrg (R) ↾_{𝑠} P = IDLsrg (R) ↾_{𝑠} PrmIdeal (R)$
7	5 1 6	3eqtr4g	$⊢ R \in Ring \to S = IDLsrg (R) ↾_{𝑠} P$
8	7	fveq2d	$⊢ R \in Ring \to TopOpen (S) = TopOpen (IDLsrg (R) ↾_{𝑠} P)$
9		eqid	$⊢ IDLsrg (R) ↾_{𝑠} P = IDLsrg (R) ↾_{𝑠} P$
10		eqid	$⊢ TopOpen (IDLsrg (R)) = TopOpen (IDLsrg (R))$
11	9 10	resstopn	$⊢ TopOpen (IDLsrg (R)) ↾_{𝑡} P = TopOpen (IDLsrg (R) ↾_{𝑠} P)$
12	8 11	eqtr4di	$⊢ R \in Ring \to TopOpen (S) = TopOpen (IDLsrg (R)) ↾_{𝑡} P$
13		eqid	$⊢ IDLsrg (R) = IDLsrg (R)$
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	$⊢ R \in Ring \to ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\}) = TopSet (IDLsrg (R))$
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	$⊢ R \in Ring \to I = {Base}_{IDLsrg (R)}$
21	20	adantr	$⊢ (R \in Ring \land i \in I) \to I = {Base}_{IDLsrg (R)}$
22	21	3ad2ant1	$⊢ ((R \in Ring \land i \in I) \land j \in I \land \neg i \subseteq j) \to I = {Base}_{IDLsrg (R)}$
23	19 22	eleqtrd	$⊢ ((R \in Ring \land i \in I) \land j \in I \land \neg i \subseteq j) \to j \in {Base}_{IDLsrg (R)}$
24	23	rabssdv	$⊢ (R \in Ring \land i \in I) \to \{j \in I \| \neg i \subseteq j\} \subseteq {Base}_{IDLsrg (R)}$
25	18 24	elpwd	$⊢ (R \in Ring \land i \in I) \to \{j \in I \| \neg i \subseteq j\} \in 𝒫 {Base}_{IDLsrg (R)}$
26	25	ralrimiva	$⊢ R \in Ring \to \forall i \in I \{j \in I \| \neg i \subseteq j\} \in 𝒫 {Base}_{IDLsrg (R)}$
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	$⊢ \forall i \in I \{j \in I \| \neg i \subseteq j\} \in 𝒫 {Base}_{IDLsrg (R)} \to ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\}) \subseteq 𝒫 {Base}_{IDLsrg (R)}$
29	26 28	syl	$⊢ R \in Ring \to ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\}) \subseteq 𝒫 {Base}_{IDLsrg (R)}$
30	15 29	eqsstrrd	$⊢ R \in Ring \to TopSet (IDLsrg (R)) \subseteq 𝒫 {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)) \subseteq 𝒫 {Base}_{IDLsrg (R)} \to TopSet (IDLsrg (R)) = TopOpen (IDLsrg (R))$
34	30 33	syl	$⊢ R \in Ring \to TopSet (IDLsrg (R)) = TopOpen (IDLsrg (R))$
35	15 34	eqtrd	$⊢ R \in Ring \to ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\}) = TopOpen (IDLsrg (R))$
36	35	oveq1d	$⊢ R \in Ring \to ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\}) ↾_{𝑡} P = TopOpen (IDLsrg (R)) ↾_{𝑡} P$
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	$⊢ R \in Ring \to PrmIdeal (R) \subseteq LIdeal (R)$
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	eqtrid	$⊢ 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	bitrid	$⊢ 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	bitrid	$⊢ 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