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

Metamath Proof Explorer

Theorem 01eq0ring

Description: If the zero and the identity element of a ring are the same, the ring is the zero ring. (Contributed by AV, 16-Apr-2019) (Proof shortened by SN, 23-Feb-2025)

		Ref	Expression
	Hypotheses	0ring.b	$⊢ B = {Base}_{R}$
		0ring.0	$⊢ \underset{˙}{0} = 0_{R}$
		0ring01eq.1	$⊢ \underset{˙}{1} = 1_{R}$
	Assertion	01eq0ring	$⊢ (R \in Ring \land \underset{˙}{0} = \underset{˙}{1}) \to B = \{\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		eqcom	$⊢ \underset{˙}{0} = \underset{˙}{1} \leftrightarrow \underset{˙}{1} = \underset{˙}{0}$
5	1 2	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in B$
6	5	ne0d	$⊢ R \in Ring \to B \neq \emptyset$
7	5	adantr	$⊢ (R \in Ring \land x \in B) \to \underset{˙}{0} \in B$
8	1 3 2	ring1eq0	$⊢ (R \in Ring \land x \in B \land \underset{˙}{0} \in B) \to (\underset{˙}{1} = \underset{˙}{0} \to x = \underset{˙}{0})$
9	7 8	mpd3an3	$⊢ (R \in Ring \land x \in B) \to (\underset{˙}{1} = \underset{˙}{0} \to x = \underset{˙}{0})$
10	9	impancom	$⊢ (R \in Ring \land \underset{˙}{1} = \underset{˙}{0}) \to (x \in B \to x = \underset{˙}{0})$
11	10	ralrimiv	$⊢ (R \in Ring \land \underset{˙}{1} = \underset{˙}{0}) \to \forall x \in B x = \underset{˙}{0}$
12		eqsn	$⊢ B \neq \emptyset \to (B = \{\underset{˙}{0}\} \leftrightarrow \forall x \in B x = \underset{˙}{0})$
13	12	biimpar	$⊢ (B \neq \emptyset \land \forall x \in B x = \underset{˙}{0}) \to B = \{\underset{˙}{0}\}$
14	6 11 13	syl2an2r	$⊢ (R \in Ring \land \underset{˙}{1} = \underset{˙}{0}) \to B = \{\underset{˙}{0}\}$
15	4 14	sylan2b	$⊢ (R \in Ring \land \underset{˙}{0} = \underset{˙}{1}) \to B = \{\underset{˙}{0}\}$