This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0ringbas

Description: The base set of a zero ring, a ring which is not a nonzero ring, is the singleton of the zero element. (Contributed by AV, 17-Apr-2020)

	Ref	Expression
Hypotheses	0ring.b	$⊢ B = {Base}_{R}$
	0ring.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	0ringbas	$⊢ R \in (Ring ∖ NzRing) \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	0ringdif	$⊢ R \in (Ring ∖ NzRing) \leftrightarrow (R \in Ring \land B = \{\underset{˙}{0}\})$
4	3	simprbi	$⊢ R \in (Ring ∖ NzRing) \to B = \{\underset{˙}{0}\}$