zar0ring

Description: The Zariski Topology of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024)

	Ref	Expression
Hypotheses	zartop.1	$⊢ S = Spec (R)$
	zartop.2	$⊢ J = TopOpen (S)$
	zar0ring.b	$⊢ B = {Base}_{R}$
Assertion	zar0ring	$⊢ (R \in Ring \land \|B\| = 1) \to J = \{\emptyset\}$

Proof

Step	Hyp	Ref	Expression
1		zartop.1	$⊢ S = Spec (R)$
2		zartop.2	$⊢ J = TopOpen (S)$
3		zar0ring.b	$⊢ B = {Base}_{R}$
4		eqid	$⊢ LIdeal (R) = LIdeal (R)$
5		eqid	$⊢ PrmIdeal (R) = PrmIdeal (R)$
6		eqid	$⊢ ran (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\}) = ran (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\})$
7	1 4 5 6	rspectopn	$⊢ R \in Ring \to ran (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\}) = TopOpen (S)$
8	7	adantr	$⊢ (R \in Ring \land \|B\| = 1) \to ran (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\}) = TopOpen (S)$
9	2 8	eqtr4id	$⊢ (R \in Ring \land \|B\| = 1) \to J = ran (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\})$
10		fvex	$⊢ PrmIdeal (R) \in V$
11	10	rabex	$⊢ \{j \in PrmIdeal (R) \| \neg i \subseteq j\} \in V$
12		eqid	$⊢ (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\}) = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\})$
13	11 12	fnmpti	$⊢ (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\}) Fn LIdeal (R)$
14	13	a1i	$⊢ (R \in Ring \land \|B\| = 1) \to (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\}) Fn LIdeal (R)$
15		eqid	$⊢ 0_{R} = 0_{R}$
16	3 15	0ringidl	$⊢ (R \in Ring \land \|B\| = 1) \to LIdeal (R) = \{\{0_{R}\}\}$
17		snex	$⊢ \{0_{R}\} \in V$
18	17	a1i	$⊢ (R \in Ring \land \|B\| = 1) \to \{0_{R}\} \in V$
19	18	snn0d	$⊢ (R \in Ring \land \|B\| = 1) \to \{\{0_{R}\}\} \neq \emptyset$
20	16 19	eqnetrd	$⊢ (R \in Ring \land \|B\| = 1) \to LIdeal (R) \neq \emptyset$
21	3	0ringprmidl	$⊢ (R \in Ring \land \|B\| = 1) \to PrmIdeal (R) = \emptyset$
22	21	rabeqdv	$⊢ (R \in Ring \land \|B\| = 1) \to \{j \in PrmIdeal (R) \| \neg i \subseteq j\} = \{j \in \emptyset \| \neg i \subseteq j\}$
23		rab0	$⊢ \{j \in \emptyset \| \neg i \subseteq j\} = \emptyset$
24	22 23	eqtrdi	$⊢ (R \in Ring \land \|B\| = 1) \to \{j \in PrmIdeal (R) \| \neg i \subseteq j\} = \emptyset$
25	24	mpteq2dv	$⊢ (R \in Ring \land \|B\| = 1) \to (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\}) = (i \in LIdeal (R) ⟼ \emptyset)$
26		fconstmpt	$⊢ LIdeal (R) \times \{\emptyset\} = (i \in LIdeal (R) ⟼ \emptyset)$
27	25 26	eqtr4di	$⊢ (R \in Ring \land \|B\| = 1) \to (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\}) = LIdeal (R) \times \{\emptyset\}$
28		fconst5	$⊢ ((i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\}) Fn LIdeal (R) \land LIdeal (R) \neq \emptyset) \to ((i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\}) = LIdeal (R) \times \{\emptyset\} \leftrightarrow ran (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\}) = \{\emptyset\})$
29	28	biimpa	$⊢ (((i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\}) Fn LIdeal (R) \land LIdeal (R) \neq \emptyset) \land (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\}) = LIdeal (R) \times \{\emptyset\}) \to ran (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\}) = \{\emptyset\}$
30	14 20 27 29	syl21anc	$⊢ (R \in Ring \land \|B\| = 1) \to ran (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| \neg i \subseteq j\}) = \{\emptyset\}$
31	9 30	eqtrd	$⊢ (R \in Ring \land \|B\| = 1) \to J = \{\emptyset\}$

Metamath Proof Explorer

Theorem zar0ring

Proof