0ring1eq0

Description: In a zero ring, a ring which is not a nonzero ring, the ring unity equals the zero element. (Contributed by AV, 17-Apr-2020)

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

Step	Hyp	Ref	Expression
1		0ring.b	$⊢ B = {Base}_{R}$
2		0ring.0	$⊢ \underset{˙}{0} = 0_{R}$
3		0ring01eq.1	$⊢ \underset{˙}{1} = 1_{R}$
4		eldif	$⊢ R \in (Ring ∖ NzRing) \leftrightarrow (R \in Ring \land \neg R \in NzRing)$
5		0ringnnzr	$⊢ R \in Ring \to (\|{Base}_{R}\| = 1 \leftrightarrow \neg R \in NzRing)$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7	6 2 3	0ring01eq	$⊢ (R \in Ring \land \|{Base}_{R}\| = 1) \to \underset{˙}{0} = \underset{˙}{1}$
8	7	eqcomd	$⊢ (R \in Ring \land \|{Base}_{R}\| = 1) \to \underset{˙}{1} = \underset{˙}{0}$
9	8	ex	$⊢ R \in Ring \to (\|{Base}_{R}\| = 1 \to \underset{˙}{1} = \underset{˙}{0})$
10	5 9	sylbird	$⊢ R \in Ring \to (\neg R \in NzRing \to \underset{˙}{1} = \underset{˙}{0})$
11	10	imp	$⊢ (R \in Ring \land \neg R \in NzRing) \to \underset{˙}{1} = \underset{˙}{0}$
12	4 11	sylbi	$⊢ R \in (Ring ∖ NzRing) \to \underset{˙}{1} = \underset{˙}{0}$

Metamath Proof Explorer