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 = Base R
0ring.0 0 ˙ = 0 R
0ring01eq.1 1 ˙ = 1 R
Assertion 0ring01eq R Ring B = 1 0 ˙ = 1 ˙

Proof

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