0ringdif

Description: A zero ring is a ring which is not a nonzero ring. (Contributed by AV, 17-Apr-2020)

	Ref	Expression
Hypotheses	0ring.b	$⊢ B = {Base}_{R}$
	0ring.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	0ringdif	$⊢ R \in (Ring ∖ NzRing) \leftrightarrow (R \in Ring \land B = \{\underset{˙}{0}\})$

Step	Hyp	Ref	Expression
1		0ring.b	$⊢ B = {Base}_{R}$
2		0ring.0	$⊢ \underset{˙}{0} = 0_{R}$
3		eldif	$⊢ R \in (Ring ∖ NzRing) \leftrightarrow (R \in Ring \land \neg R \in NzRing)$
4	1	a1i	$⊢ R \in Ring \to B = {Base}_{R}$
5	4	fveqeq2d	$⊢ R \in Ring \to (\|B\| = 1 \leftrightarrow \|{Base}_{R}\| = 1)$
6	1 2	0ring	$⊢ (R \in Ring \land \|B\| = 1) \to B = \{\underset{˙}{0}\}$
7	6	ex	$⊢ R \in Ring \to (\|B\| = 1 \to B = \{\underset{˙}{0}\})$
8		fveq2	$⊢ B = \{\underset{˙}{0}\} \to \|B\| = \|\{\underset{˙}{0}\}\|$
9	2	fvexi	$⊢ \underset{˙}{0} \in V$
10		hashsng	$⊢ \underset{˙}{0} \in V \to \|\{\underset{˙}{0}\}\| = 1$
11	9 10	ax-mp	$⊢ \|\{\underset{˙}{0}\}\| = 1$
12	8 11	eqtrdi	$⊢ B = \{\underset{˙}{0}\} \to \|B\| = 1$
13	7 12	impbid1	$⊢ R \in Ring \to (\|B\| = 1 \leftrightarrow B = \{\underset{˙}{0}\})$
14		0ringnnzr	$⊢ R \in Ring \to (\|{Base}_{R}\| = 1 \leftrightarrow \neg R \in NzRing)$
15	5 13 14	3bitr3rd	$⊢ R \in Ring \to (\neg R \in NzRing \leftrightarrow B = \{\underset{˙}{0}\})$
16	15	pm5.32i	$⊢ (R \in Ring \land \neg R \in NzRing) \leftrightarrow (R \in Ring \land B = \{\underset{˙}{0}\})$
17	3 16	bitri	$⊢ R \in (Ring ∖ NzRing) \leftrightarrow (R \in Ring \land B = \{\underset{˙}{0}\})$

Metamath Proof Explorer