Metamath Proof Explorer


Theorem 0ring01eq

Description: In a ring with only one element, i.e. a zero ring, the zero and the identity element are the same. (Contributed by AV, 14-Apr-2019)

Ref Expression
Hypotheses 0ring.b B=BaseR
0ring.0 0˙=0R
0ring01eq.1 1˙=1R
Assertion 0ring01eq RRingB=10˙=1˙

Proof

Step Hyp Ref Expression
1 0ring.b B=BaseR
2 0ring.0 0˙=0R
3 0ring01eq.1 1˙=1R
4 1 2 0ring RRingB=1B=0˙
5 1 3 ringidcl RRing1˙B
6 eleq2 B=0˙1˙B1˙0˙
7 elsni 1˙0˙1˙=0˙
8 7 eqcomd 1˙0˙0˙=1˙
9 6 8 syl6bi B=0˙1˙B0˙=1˙
10 5 9 syl5com RRingB=0˙0˙=1˙
11 10 adantr RRingB=1B=0˙0˙=1˙
12 4 11 mpd RRingB=10˙=1˙