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=BaseR
ring1ne0.u 1˙=1R
ring1ne0.z 0˙=0R
Assertion ring1ne0 RRing1<B1˙0˙

Proof

Step Hyp Ref Expression
1 ring1ne0.b B=BaseR
2 ring1ne0.u 1˙=1R
3 ring1ne0.z 0˙=0R
4 1 fvexi BV
5 hashgt12el BV1<BxByBxy
6 4 5 mpan 1<BxByBxy
7 6 adantl RRing1<BxByBxy
8 1 2 3 ring1eq0 RRingxByB1˙=0˙x=y
9 8 necon3d RRingxByBxy1˙0˙
10 9 3expib RRingxByBxy1˙0˙
11 10 adantr RRing1<BxByBxy1˙0˙
12 11 com3l xByBxyRRing1<B1˙0˙
13 12 rexlimivv xByBxyRRing1<B1˙0˙
14 7 13 mpcom RRing1<B1˙0˙