0ring

Description: If a ring has only one element, it is the zero ring. According to Wikipedia ("Zero ring", 14-Apr-2019, https://en.wikipedia.org/wiki/Zero_ring): "The zero ring, denoted {0} or simply 0, consists of the one-element set {0} with the operations + and * defined so that 0 + 0 = 0 and 0 * 0 = 0.". (Contributed by AV, 14-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		0ring.b	$⊢ B = {Base}_{R}$
2		0ring.0	$⊢ \underset{˙}{0} = 0_{R}$
3	1 2	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in B$
4	1	fvexi	$⊢ B \in V$
5		hashen1	$⊢ B \in V \to (\|B\| = 1 \leftrightarrow B \approx 1_{𝑜})$
6	4 5	ax-mp	$⊢ \|B\| = 1 \leftrightarrow B \approx 1_{𝑜}$
7		en1eqsn	$⊢ (\underset{˙}{0} \in B \land B \approx 1_{𝑜}) \to B = \{\underset{˙}{0}\}$
8	7	ex	$⊢ \underset{˙}{0} \in B \to (B \approx 1_{𝑜} \to B = \{\underset{˙}{0}\})$
9	6 8	biimtrid	$⊢ \underset{˙}{0} \in B \to (\|B\| = 1 \to B = \{\underset{˙}{0}\})$
10	3 9	syl	$⊢ R \in Ring \to (\|B\| = 1 \to B = \{\underset{˙}{0}\})$
11	10	imp	$⊢ (R \in Ring \land \|B\| = 1) \to B = \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem 0ring

Proof