0ringprmidl

Description: The trivial ring does not have any prime ideal. (Contributed by Thierry Arnoux, 30-Jun-2024)

		Ref	Expression
	Hypothesis	0ringprmidl.1	$⊢ B = {Base}_{R}$
	Assertion	0ringprmidl	$⊢ (R \in Ring \land \|B\| = 1) \to PrmIdeal (R) = \emptyset$

Step	Hyp	Ref	Expression
1		0ringprmidl.1	$⊢ B = {Base}_{R}$
2		prmidlssidl	$⊢ R \in Ring \to PrmIdeal (R) \subseteq LIdeal (R)$
3	2	adantr	$⊢ (R \in Ring \land \|B\| = 1) \to PrmIdeal (R) \subseteq LIdeal (R)$
4		eqid	$⊢ 0_{R} = 0_{R}$
5	1 4	0ringidl	$⊢ (R \in Ring \land \|B\| = 1) \to LIdeal (R) = \{\{0_{R}\}\}$
6	3 5	sseqtrd	$⊢ (R \in Ring \land \|B\| = 1) \to PrmIdeal (R) \subseteq \{\{0_{R}\}\}$
7	6	sselda	$⊢ ((R \in Ring \land \|B\| = 1) \land i \in PrmIdeal (R)) \to i \in \{\{0_{R}\}\}$
8		elsni	$⊢ i \in \{\{0_{R}\}\} \to i = \{0_{R}\}$
9	7 8	syl	$⊢ ((R \in Ring \land \|B\| = 1) \land i \in PrmIdeal (R)) \to i = \{0_{R}\}$
10		eqid	$⊢ \cdot_{R} = \cdot_{R}$
11	1 10	prmidlnr	$⊢ (R \in Ring \land i \in PrmIdeal (R)) \to i \neq B$
12	11	adantlr	$⊢ ((R \in Ring \land \|B\| = 1) \land i \in PrmIdeal (R)) \to i \neq B$
13	1 4	0ring	$⊢ (R \in Ring \land \|B\| = 1) \to B = \{0_{R}\}$
14	13	adantr	$⊢ ((R \in Ring \land \|B\| = 1) \land i \in PrmIdeal (R)) \to B = \{0_{R}\}$
15	12 14	neeqtrd	$⊢ ((R \in Ring \land \|B\| = 1) \land i \in PrmIdeal (R)) \to i \neq \{0_{R}\}$
16	15	neneqd	$⊢ ((R \in Ring \land \|B\| = 1) \land i \in PrmIdeal (R)) \to \neg i = \{0_{R}\}$
17	9 16	pm2.65da	$⊢ (R \in Ring \land \|B\| = 1) \to \neg i \in PrmIdeal (R)$
18	17	eq0rdv	$⊢ (R \in Ring \land \|B\| = 1) \to PrmIdeal (R) = \emptyset$

Metamath Proof Explorer