Metamath Proof Explorer


Theorem 01eq0ring

Description: If the zero and the identity element of a ring are the same, the ring is the zero ring. (Contributed by AV, 16-Apr-2019) (Proof shortened by SN, 23-Feb-2025)

Ref Expression
Hypotheses 0ring.b B=BaseR
0ring.0 0˙=0R
0ring01eq.1 1˙=1R
Assertion 01eq0ring RRing0˙=1˙B=0˙

Proof

Step Hyp Ref Expression
1 0ring.b B=BaseR
2 0ring.0 0˙=0R
3 0ring01eq.1 1˙=1R
4 eqcom 0˙=1˙1˙=0˙
5 1 2 ring0cl RRing0˙B
6 5 ne0d RRingB
7 5 adantr RRingxB0˙B
8 1 3 2 ring1eq0 RRingxB0˙B1˙=0˙x=0˙
9 7 8 mpd3an3 RRingxB1˙=0˙x=0˙
10 9 impancom RRing1˙=0˙xBx=0˙
11 10 ralrimiv RRing1˙=0˙xBx=0˙
12 eqsn BB=0˙xBx=0˙
13 12 biimpar BxBx=0˙B=0˙
14 6 11 13 syl2an2r RRing1˙=0˙B=0˙
15 4 14 sylan2b RRing0˙=1˙B=0˙