Description: A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 22-Dec-2013) (Revised by AV, 24-Aug-2021) (Proof shortened by AV, 1-Feb-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ringadd2.b | |
|
ringadd2.p | |
||
ringadd2.t | |
||
Assertion | ringadd2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringadd2.b | |
|
2 | ringadd2.p | |
|
3 | ringadd2.t | |
|
4 | eqid | |
|
5 | 1 4 | ringidcl | |
6 | 5 | adantr | |
7 | simpr | |
|
8 | 7 7 | oveq12d | |
9 | 8 | oveq1d | |
10 | 9 | eqeq2d | |
11 | 1 2 3 4 | ringo2times | |
12 | 6 10 11 | rspcedvd | |