0ring01eqbi

Description: In a unital ring the zero equals the unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010) (Revised by AV, 23-Jan-2020)

	Ref	Expression
Hypotheses	0ring.b	$⊢ B = {Base}_{R}$
	0ring.0	$⊢ \underset{˙}{0} = 0_{R}$
	0ring01eq.1	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	0ring01eqbi	$⊢ R \in Ring \to (B \approx 1_{𝑜} \leftrightarrow \underset{˙}{1} = \underset{˙}{0})$

Proof

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	1	fvexi	$⊢ B \in V$
5		hashen1	$⊢ B \in V \to (\|B\| = 1 \leftrightarrow B \approx 1_{𝑜})$
6	4 5	mp1i	$⊢ R \in Ring \to (\|B\| = 1 \leftrightarrow B \approx 1_{𝑜})$
7	1 2 3	0ring01eq	$⊢ (R \in Ring \land \|B\| = 1) \to \underset{˙}{0} = \underset{˙}{1}$
8	7	eqcomd	$⊢ (R \in Ring \land \|B\| = 1) \to \underset{˙}{1} = \underset{˙}{0}$
9	8	ex	$⊢ R \in Ring \to (\|B\| = 1 \to \underset{˙}{1} = \underset{˙}{0})$
10		eqcom	$⊢ \underset{˙}{1} = \underset{˙}{0} \leftrightarrow \underset{˙}{0} = \underset{˙}{1}$
11	1 2 3	01eq0ring	$⊢ (R \in Ring \land \underset{˙}{0} = \underset{˙}{1}) \to B = \{\underset{˙}{0}\}$
12		fveq2	$⊢ B = \{\underset{˙}{0}\} \to \|B\| = \|\{\underset{˙}{0}\}\|$
13	2	fvexi	$⊢ \underset{˙}{0} \in V$
14		hashsng	$⊢ \underset{˙}{0} \in V \to \|\{\underset{˙}{0}\}\| = 1$
15	13 14	mp1i	$⊢ B = \{\underset{˙}{0}\} \to \|\{\underset{˙}{0}\}\| = 1$
16	12 15	eqtrd	$⊢ B = \{\underset{˙}{0}\} \to \|B\| = 1$
17	11 16	syl	$⊢ (R \in Ring \land \underset{˙}{0} = \underset{˙}{1}) \to \|B\| = 1$
18	17	ex	$⊢ R \in Ring \to (\underset{˙}{0} = \underset{˙}{1} \to \|B\| = 1)$
19	10 18	biimtrid	$⊢ R \in Ring \to (\underset{˙}{1} = \underset{˙}{0} \to \|B\| = 1)$
20	9 19	impbid	$⊢ R \in Ring \to (\|B\| = 1 \leftrightarrow \underset{˙}{1} = \underset{˙}{0})$
21	6 20	bitr3d	$⊢ R \in Ring \to (B \approx 1_{𝑜} \leftrightarrow \underset{˙}{1} = \underset{˙}{0})$

Metamath Proof Explorer

Theorem 0ring01eqbi

Proof