Metamath Proof Explorer


Theorem ringadd2

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 B=BaseR
ringadd2.p +˙=+R
ringadd2.t ·˙=R
Assertion ringadd2 RRingXBxBX+˙X=x+˙x·˙X

Proof

Step Hyp Ref Expression
1 ringadd2.b B=BaseR
2 ringadd2.p +˙=+R
3 ringadd2.t ·˙=R
4 eqid 1R=1R
5 1 4 ringidcl RRing1RB
6 5 adantr RRingXB1RB
7 simpr RRingXBx=1Rx=1R
8 7 7 oveq12d RRingXBx=1Rx+˙x=1R+˙1R
9 8 oveq1d RRingXBx=1Rx+˙x·˙X=1R+˙1R·˙X
10 9 eqeq2d RRingXBx=1RX+˙X=x+˙x·˙XX+˙X=1R+˙1R·˙X
11 1 2 3 4 ringo2times RRingXBX+˙X=1R+˙1R·˙X
12 6 10 11 rspcedvd RRingXBxBX+˙X=x+˙x·˙X