ring1ne0

Description: If a ring has at least two elements, its one and zero are different. (Contributed by AV, 13-Apr-2019)

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

Step	Hyp	Ref	Expression
1		ring1ne0.b	$⊢ B = {Base}_{R}$
2		ring1ne0.u	$⊢ \underset{˙}{1} = 1_{R}$
3		ring1ne0.z	$⊢ \underset{˙}{0} = 0_{R}$
4	1	fvexi	$⊢ B \in V$
5		hashgt12el	$⊢ (B \in V \land 1 < \|B\|) \to \exists x \in B \exists y \in B x \neq y$
6	4 5	mpan	$⊢ 1 < \|B\| \to \exists x \in B \exists y \in B x \neq y$
7	6	adantl	$⊢ (R \in Ring \land 1 < \|B\|) \to \exists x \in B \exists y \in B x \neq y$
8	1 2 3	ring1eq0	$⊢ (R \in Ring \land x \in B \land y \in B) \to (\underset{˙}{1} = \underset{˙}{0} \to x = y)$
9	8	necon3d	$⊢ (R \in Ring \land x \in B \land y \in B) \to (x \neq y \to \underset{˙}{1} \neq \underset{˙}{0})$
10	9	3expib	$⊢ R \in Ring \to ((x \in B \land y \in B) \to (x \neq y \to \underset{˙}{1} \neq \underset{˙}{0}))$
11	10	adantr	$⊢ (R \in Ring \land 1 < \|B\|) \to ((x \in B \land y \in B) \to (x \neq y \to \underset{˙}{1} \neq \underset{˙}{0}))$
12	11	com3l	$⊢ (x \in B \land y \in B) \to (x \neq y \to ((R \in Ring \land 1 < \|B\|) \to \underset{˙}{1} \neq \underset{˙}{0}))$
13	12	rexlimivv	$⊢ \exists x \in B \exists y \in B x \neq y \to ((R \in Ring \land 1 < \|B\|) \to \underset{˙}{1} \neq \underset{˙}{0})$
14	7 13	mpcom	$⊢ (R \in Ring \land 1 < \|B\|) \to \underset{˙}{1} \neq \underset{˙}{0}$

Metamath Proof Explorer