zarcls

Description: The open sets of the Zariski topology are the complements of the closed sets. (Contributed by Thierry Arnoux, 16-Jun-2024)

	Ref	Expression
Hypotheses	zartop.1	$⊢ S = Spec (R)$
	zartop.2	$⊢ J = TopOpen (S)$
	zarcls.1	$⊢ P = PrmIdeal (R)$
	zarcls.2	$⊢ V = (i \in LIdeal (R) ⟼ \{j \in P \| i \subseteq j\})$
Assertion	zarcls	$⊢ R \in Ring \to J = \{s \in 𝒫 P \| P ∖ s \in ran V\}$

Proof

Step	Hyp	Ref	Expression
1		zartop.1	$⊢ S = Spec (R)$
2		zartop.2	$⊢ J = TopOpen (S)$
3		zarcls.1	$⊢ P = PrmIdeal (R)$
4		zarcls.2	$⊢ V = (i \in LIdeal (R) ⟼ \{j \in P \| i \subseteq j\})$
5		eqid	$⊢ LIdeal (R) = LIdeal (R)$
6		eqid	$⊢ ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\}) = ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\})$
7	1 5 3 6	rspectopn	$⊢ R \in Ring \to ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\}) = TopOpen (S)$
8	2 7	eqtr4id	$⊢ R \in Ring \to J = ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\})$
9		nfv	$⊢ Ⅎ s R \in Ring$
10		nfcv	$⊢ \underline{Ⅎ} s ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\})$
11		nfrab1	$⊢ \underline{Ⅎ} s \{s \in 𝒫 P \| P ∖ s \in ran V\}$
12		notrab	$⊢ P ∖ \{j \in P \| i \subseteq j\} = \{j \in P \| \neg i \subseteq j\}$
13	12	eqeq2i	$⊢ s = P ∖ \{j \in P \| i \subseteq j\} \leftrightarrow s = \{j \in P \| \neg i \subseteq j\}$
14		ssrab2	$⊢ \{j \in P \| i \subseteq j\} \subseteq P$
15	14	a1i	$⊢ s \in 𝒫 P \to \{j \in P \| i \subseteq j\} \subseteq P$
16		elpwi	$⊢ s \in 𝒫 P \to s \subseteq P$
17		ssdifsym	$⊢ (\{j \in P \| i \subseteq j\} \subseteq P \land s \subseteq P) \to (s = P ∖ \{j \in P \| i \subseteq j\} \leftrightarrow \{j \in P \| i \subseteq j\} = P ∖ s)$
18	15 16 17	syl2anc	$⊢ s \in 𝒫 P \to (s = P ∖ \{j \in P \| i \subseteq j\} \leftrightarrow \{j \in P \| i \subseteq j\} = P ∖ s)$
19		eqcom	$⊢ \{j \in P \| i \subseteq j\} = P ∖ s \leftrightarrow P ∖ s = \{j \in P \| i \subseteq j\}$
20	18 19	bitrdi	$⊢ s \in 𝒫 P \to (s = P ∖ \{j \in P \| i \subseteq j\} \leftrightarrow P ∖ s = \{j \in P \| i \subseteq j\})$
21	13 20	bitr3id	$⊢ s \in 𝒫 P \to (s = \{j \in P \| \neg i \subseteq j\} \leftrightarrow P ∖ s = \{j \in P \| i \subseteq j\})$
22	21	ad2antlr	$⊢ ((R \in Ring \land s \in 𝒫 P) \land i \in LIdeal (R)) \to (s = \{j \in P \| \neg i \subseteq j\} \leftrightarrow P ∖ s = \{j \in P \| i \subseteq j\})$
23	22	rexbidva	$⊢ (R \in Ring \land s \in 𝒫 P) \to (\exists i \in LIdeal (R) s = \{j \in P \| \neg i \subseteq j\} \leftrightarrow \exists i \in LIdeal (R) P ∖ s = \{j \in P \| i \subseteq j\})$
24	3	fvexi	$⊢ P \in V$
25	24	rabex	$⊢ \{j \in P \| i \subseteq j\} \in V$
26	4 25	elrnmpti	$⊢ P ∖ s \in ran V \leftrightarrow \exists i \in LIdeal (R) P ∖ s = \{j \in P \| i \subseteq j\}$
27	23 26	bitr4di	$⊢ (R \in Ring \land s \in 𝒫 P) \to (\exists i \in LIdeal (R) s = \{j \in P \| \neg i \subseteq j\} \leftrightarrow P ∖ s \in ran V)$
28	27	pm5.32da	$⊢ R \in Ring \to ((s \in 𝒫 P \land \exists i \in LIdeal (R) s = \{j \in P \| \neg i \subseteq j\}) \leftrightarrow (s \in 𝒫 P \land P ∖ s \in ran V))$
29		ssrab2	$⊢ \{j \in P \| \neg i \subseteq j\} \subseteq P$
30	24	elpw2	$⊢ \{j \in P \| \neg i \subseteq j\} \in 𝒫 P \leftrightarrow \{j \in P \| \neg i \subseteq j\} \subseteq P$
31	29 30	mpbir	$⊢ \{j \in P \| \neg i \subseteq j\} \in 𝒫 P$
32	31	rgenw	$⊢ \forall i \in LIdeal (R) \{j \in P \| \neg i \subseteq j\} \in 𝒫 P$
33		eqid	$⊢ (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\}) = (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\})$
34	33	rnmptss	$⊢ \forall i \in LIdeal (R) \{j \in P \| \neg i \subseteq j\} \in 𝒫 P \to ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\}) \subseteq 𝒫 P$
35	32 34	ax-mp	$⊢ ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\}) \subseteq 𝒫 P$
36	35	sseli	$⊢ s \in ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\}) \to s \in 𝒫 P$
37	36	pm4.71ri	$⊢ s \in ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\}) \leftrightarrow (s \in 𝒫 P \land s \in ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\}))$
38		vex	$⊢ s \in V$
39	33	elrnmpt	$⊢ s \in V \to (s \in ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\}) \leftrightarrow \exists i \in LIdeal (R) s = \{j \in P \| \neg i \subseteq j\})$
40	38 39	ax-mp	$⊢ s \in ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\}) \leftrightarrow \exists i \in LIdeal (R) s = \{j \in P \| \neg i \subseteq j\}$
41	40	anbi2i	$⊢ (s \in 𝒫 P \land s \in ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\})) \leftrightarrow (s \in 𝒫 P \land \exists i \in LIdeal (R) s = \{j \in P \| \neg i \subseteq j\})$
42	37 41	bitri	$⊢ s \in ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\}) \leftrightarrow (s \in 𝒫 P \land \exists i \in LIdeal (R) s = \{j \in P \| \neg i \subseteq j\})$
43		rabid	$⊢ s \in \{s \in 𝒫 P \| P ∖ s \in ran V\} \leftrightarrow (s \in 𝒫 P \land P ∖ s \in ran V)$
44	28 42 43	3bitr4g	$⊢ R \in Ring \to (s \in ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\}) \leftrightarrow s \in \{s \in 𝒫 P \| P ∖ s \in ran V\})$
45	9 10 11 44	eqrd	$⊢ R \in Ring \to ran (i \in LIdeal (R) ⟼ \{j \in P \| \neg i \subseteq j\}) = \{s \in 𝒫 P \| P ∖ s \in ran V\}$
46	8 45	eqtrd	$⊢ R \in Ring \to J = \{s \in 𝒫 P \| P ∖ s \in ran V\}$

Metamath Proof Explorer

Theorem zarcls

Proof