ring1eq0

Description: If one and zero are equal, then any two elements of a ring are equal. Alternately, every ring has one distinct from zero except the zero ring containing the single element { 0 } . (Contributed by Mario Carneiro, 10-Sep-2014)

	Ref	Expression
Hypotheses	ring1eq0.b	$⊢ B = {Base}_{R}$
	ring1eq0.u	$⊢ \underset{˙}{1} = 1_{R}$
	ring1eq0.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	ring1eq0	$⊢ (R \in Ring \land X \in B \land Y \in B) \to (\underset{˙}{1} = \underset{˙}{0} \to X = Y)$

Proof

Step	Hyp	Ref	Expression
1		ring1eq0.b	$⊢ B = {Base}_{R}$
2		ring1eq0.u	$⊢ \underset{˙}{1} = 1_{R}$
3		ring1eq0.z	$⊢ \underset{˙}{0} = 0_{R}$
4		simpr	$⊢ ((R \in Ring \land X \in B \land Y \in B) \land \underset{˙}{1} = \underset{˙}{0}) \to \underset{˙}{1} = \underset{˙}{0}$
5	4	oveq1d	$⊢ ((R \in Ring \land X \in B \land Y \in B) \land \underset{˙}{1} = \underset{˙}{0}) \to \underset{˙}{1} \cdot_{R} X = \underset{˙}{0} \cdot_{R} X$
6	4	oveq1d	$⊢ ((R \in Ring \land X \in B \land Y \in B) \land \underset{˙}{1} = \underset{˙}{0}) \to \underset{˙}{1} \cdot_{R} Y = \underset{˙}{0} \cdot_{R} Y$
7		simpl1	$⊢ ((R \in Ring \land X \in B \land Y \in B) \land \underset{˙}{1} = \underset{˙}{0}) \to R \in Ring$
8		simpl2	$⊢ ((R \in Ring \land X \in B \land Y \in B) \land \underset{˙}{1} = \underset{˙}{0}) \to X \in B$
9		eqid	$⊢ \cdot_{R} = \cdot_{R}$
10	1 9 3	ringlz	$⊢ (R \in Ring \land X \in B) \to \underset{˙}{0} \cdot_{R} X = \underset{˙}{0}$
11	7 8 10	syl2anc	$⊢ ((R \in Ring \land X \in B \land Y \in B) \land \underset{˙}{1} = \underset{˙}{0}) \to \underset{˙}{0} \cdot_{R} X = \underset{˙}{0}$
12		simpl3	$⊢ ((R \in Ring \land X \in B \land Y \in B) \land \underset{˙}{1} = \underset{˙}{0}) \to Y \in B$
13	1 9 3	ringlz	$⊢ (R \in Ring \land Y \in B) \to \underset{˙}{0} \cdot_{R} Y = \underset{˙}{0}$
14	7 12 13	syl2anc	$⊢ ((R \in Ring \land X \in B \land Y \in B) \land \underset{˙}{1} = \underset{˙}{0}) \to \underset{˙}{0} \cdot_{R} Y = \underset{˙}{0}$
15	11 14	eqtr4d	$⊢ ((R \in Ring \land X \in B \land Y \in B) \land \underset{˙}{1} = \underset{˙}{0}) \to \underset{˙}{0} \cdot_{R} X = \underset{˙}{0} \cdot_{R} Y$
16	6 15	eqtr4d	$⊢ ((R \in Ring \land X \in B \land Y \in B) \land \underset{˙}{1} = \underset{˙}{0}) \to \underset{˙}{1} \cdot_{R} Y = \underset{˙}{0} \cdot_{R} X$
17	5 16	eqtr4d	$⊢ ((R \in Ring \land X \in B \land Y \in B) \land \underset{˙}{1} = \underset{˙}{0}) \to \underset{˙}{1} \cdot_{R} X = \underset{˙}{1} \cdot_{R} Y$
18	1 9 2	ringlidm	$⊢ (R \in Ring \land X \in B) \to \underset{˙}{1} \cdot_{R} X = X$
19	7 8 18	syl2anc	$⊢ ((R \in Ring \land X \in B \land Y \in B) \land \underset{˙}{1} = \underset{˙}{0}) \to \underset{˙}{1} \cdot_{R} X = X$
20	1 9 2	ringlidm	$⊢ (R \in Ring \land Y \in B) \to \underset{˙}{1} \cdot_{R} Y = Y$
21	7 12 20	syl2anc	$⊢ ((R \in Ring \land X \in B \land Y \in B) \land \underset{˙}{1} = \underset{˙}{0}) \to \underset{˙}{1} \cdot_{R} Y = Y$
22	17 19 21	3eqtr3d	$⊢ ((R \in Ring \land X \in B \land Y \in B) \land \underset{˙}{1} = \underset{˙}{0}) \to X = Y$
23	22	ex	$⊢ (R \in Ring \land X \in B \land Y \in B) \to (\underset{˙}{1} = \underset{˙}{0} \to X = Y)$

Metamath Proof Explorer

Theorem ring1eq0

Proof