Metamath Proof Explorer


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 = Base R
ring1ne0.u 1 ˙ = 1 R
ring1ne0.z 0 ˙ = 0 R
Assertion ring1ne0 R Ring 1 < B 1 ˙ 0 ˙

Proof

Step Hyp Ref Expression
1 ring1ne0.b B = Base R
2 ring1ne0.u 1 ˙ = 1 R
3 ring1ne0.z 0 ˙ = 0 R
4 1 fvexi B V
5 hashgt12el B V 1 < B x B y B x y
6 4 5 mpan 1 < B x B y B x y
7 6 adantl R Ring 1 < B x B y B x y
8 1 2 3 ring1eq0 R Ring x B y B 1 ˙ = 0 ˙ x = y
9 8 necon3d R Ring x B y B x y 1 ˙ 0 ˙
10 9 3expib R Ring x B y B x y 1 ˙ 0 ˙
11 10 adantr R Ring 1 < B x B y B x y 1 ˙ 0 ˙
12 11 com3l x B y B x y R Ring 1 < B 1 ˙ 0 ˙
13 12 rexlimivv x B y B x y R Ring 1 < B 1 ˙ 0 ˙
14 7 13 mpcom R Ring 1 < B 1 ˙ 0 ˙