0ringidl

Description: The zero ideal is the only ideal of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024)

	Ref	Expression
Hypotheses	0ringidl.1	$⊢ B = {Base}_{R}$
	0ringidl.2	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	0ringidl	$⊢ (R \in Ring \land \|B\| = 1) \to LIdeal (R) = \{\{\underset{˙}{0}\}\}$

Step	Hyp	Ref	Expression
1		0ringidl.1	$⊢ B = {Base}_{R}$
2		0ringidl.2	$⊢ \underset{˙}{0} = 0_{R}$
3		eqid	$⊢ LIdeal (R) = LIdeal (R)$
4	1 3	lidlss	$⊢ i \in LIdeal (R) \to i \subseteq B$
5	4	adantl	$⊢ ((R \in Ring \land \|B\| = 1) \land i \in LIdeal (R)) \to i \subseteq B$
6	1 2	0ring	$⊢ (R \in Ring \land \|B\| = 1) \to B = \{\underset{˙}{0}\}$
7	6	adantr	$⊢ ((R \in Ring \land \|B\| = 1) \land i \in LIdeal (R)) \to B = \{\underset{˙}{0}\}$
8	5 7	sseqtrd	$⊢ ((R \in Ring \land \|B\| = 1) \land i \in LIdeal (R)) \to i \subseteq \{\underset{˙}{0}\}$
9	3 2	lidl0cl	$⊢ (R \in Ring \land i \in LIdeal (R)) \to \underset{˙}{0} \in i$
10	9	adantlr	$⊢ ((R \in Ring \land \|B\| = 1) \land i \in LIdeal (R)) \to \underset{˙}{0} \in i$
11	10	snssd	$⊢ ((R \in Ring \land \|B\| = 1) \land i \in LIdeal (R)) \to \{\underset{˙}{0}\} \subseteq i$
12	8 11	eqssd	$⊢ ((R \in Ring \land \|B\| = 1) \land i \in LIdeal (R)) \to i = \{\underset{˙}{0}\}$
13	3 2	lidl0	$⊢ R \in Ring \to \{\underset{˙}{0}\} \in LIdeal (R)$
14	13	adantr	$⊢ (R \in Ring \land \|B\| = 1) \to \{\underset{˙}{0}\} \in LIdeal (R)$
15	12 14	eqsnd	$⊢ (R \in Ring \land \|B\| = 1) \to LIdeal (R) = \{\{\underset{˙}{0}\}\}$

Metamath Proof Explorer