Theorem 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={\mathrm{Base}}_R$$
	ring1ne0.u	$$⊢\underset{\dot{}}{1}=1_R$$
	ring1ne0.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	ring1ne0	$$⊢\left(R\in \mathrm{Ring}\wedge 1<\left|B\right|\right)\to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$

Proof

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