0ring01eq

Description: In a ring with only one element, i.e. a zero ring, the zero and the identity element are the same. (Contributed by AV, 14-Apr-2019)

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

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 2	0ring	$⊢ (R \in Ring \land \|B\| = 1) \to B = \{\underset{˙}{0}\}$
5	1 3	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in B$
6		eleq2	$⊢ B = \{\underset{˙}{0}\} \to (\underset{˙}{1} \in B \leftrightarrow \underset{˙}{1} \in \{\underset{˙}{0}\})$
7		elsni	$⊢ \underset{˙}{1} \in \{\underset{˙}{0}\} \to \underset{˙}{1} = \underset{˙}{0}$
8	7	eqcomd	$⊢ \underset{˙}{1} \in \{\underset{˙}{0}\} \to \underset{˙}{0} = \underset{˙}{1}$
9	6 8	biimtrdi	$⊢ B = \{\underset{˙}{0}\} \to (\underset{˙}{1} \in B \to \underset{˙}{0} = \underset{˙}{1})$
10	5 9	syl5com	$⊢ R \in Ring \to (B = \{\underset{˙}{0}\} \to \underset{˙}{0} = \underset{˙}{1})$
11	10	adantr	$⊢ (R \in Ring \land \|B\| = 1) \to (B = \{\underset{˙}{0}\} \to \underset{˙}{0} = \underset{˙}{1})$
12	4 11	mpd	$⊢ (R \in Ring \land \|B\| = 1) \to \underset{˙}{0} = \underset{˙}{1}$

Metamath Proof Explorer