# Is there a short proof of $x^2=(-x)^2$ in an arbitrary ring?

Identity: Let $R$ be a ring and $x \in R$. Then $x^2=(-x)^2.$

It's exam marking time here, and one of the students used the above identity in a proof. The identity is true, but I can't think of a straightforward proof of this.

Question: Is there a short proof of this identity? (Note: $R$ might not have a multiplicative identity.)

Here's a proof generated by Prover9, which makes me think there might not be a shorter proof. However, this might not necessarily be true, since Prover9 can only work with the ring theory axioms I input (and would have to prove any auxiliary lemmata we would take for granted).

============================== PROOF =================================

% Proof 1 at 0.01 (+ 0.00) seconds.
% Length of proof is 26.
% Level of proof is 10.
% Maximum clause weight is 16.
% Given clauses 30.

1 x * x = -x * -x # label(non_clause) # label(goal).  [goal].
2 x + (y + z) = (x + y) + z.  [assumption].
3 (x + y) + z = x + (y + z).  [copy(2),flip(a)].
4 x + 0 = x.  [assumption].
5 0 + x = x.  [assumption].
6 x + -x = 0.  [assumption].
8 x + y = y + x.  [assumption].
10 x * (y + z) = (x * y) + (x * z).  [assumption].
11 (x + y) * z = (x * z) + (y * z).  [assumption].
12 -c1 * -c1 != c1 * c1.  [deny(1)].
13 x + (-x + y) = y.  [para(6(a,1),3(a,1,1)),rewrite([5(2)]),flip(a)].
18 (x * 0) + (x * y) = x * y.  [para(5(a,1),10(a,1,2)),flip(a)].
19 (x * y) + (x * -y) = x * 0.  [para(6(a,1),10(a,1,2)),flip(a)].
24 --x = x.  [para(6(a,1),13(a,1,2)),rewrite([4(2)]),flip(a)].
25 x + (y + -x) = y.  [para(8(a,1),13(a,1,2))].
27 (x * y) + ((-x * y) + (z * y)) = z * y.  [para(13(a,1),11(a,1,1)),rewrite([11(5)]),flip(a)].
33 -x + (y + x) = y.  [para(24(a,1),25(a,1,2,2))].
40 x + -(x + y) = -y.  [para(33(a,1),33(a,1,2)),rewrite([8(3)])].
57 -(x + y) = -y + -x.  [para(33(a,1),40(a,1,2,1)),flip(a)].
69 x * 0 = 0.  [para(18(a,1),33(a,1,2)),rewrite([8(4),6(4)]),flip(a)].
70 (x * y) + (x * -y) = 0.  [back_rewrite(19),rewrite([69(6)])].
78 -(x * -y) = x * y.  [para(70(a,1),33(a,1,2)),rewrite([8(5),5(5)])].
87 x * -y = -(x * y).  [para(78(a,1),24(a,1,1)),flip(a)].
88 -(-c1 * c1) != c1 * c1.  [back_rewrite(12),rewrite([87(5)])].
101 -(-x * y) = x * y.  [para(27(a,1),33(a,1,2)),rewrite([57(5),8(8),13(8)])].
102 $F. [resolve(101,a,88,a)]. ============================== end of proof ==========================  ## 5 Answers Let$\rm\:y=x\:$in the Law of Signs:$\rm\:xy = xy+(x+-x)(-y) = x(y+-y) + (-x)(-y) = (-x)(-y)$Remark$\ $The proof has the following conceptual intepretation:$\rm\:xy = (-x)(-y)\:$since they are both additive inverses of$\rm\:x(-y)\:hence are equal by uniqueness of inverses. As I frequently emphasize, uniqueness theorems provide powerful tools for proving equalities. • Boy do you emphasize on that often! Nice link... you made your point! Commented Nov 1, 2012 at 6:54 \begin{align} 0=(x-x)^2 &= x^2+x(-x)+(-x)x+(-x)^2 \\ &= x^2+x(-x)+(-x)x+x^2-x^2+(-x)^2 \\ &= x(x-x)+(-x+x)x-x^2+(-x)^2 \\ &= -x^2+(-x)^2 \end{align} • Great! This is exactly what I'm after. Thanks (and thanks to the other answerers too). Commented Nov 1, 2012 at 1:20 • @DouglasS.Stones: Bill Dubuque just posted a far superior answer - please take a look! – wj32 Commented Nov 1, 2012 at 1:31 • I agree, it is very insightful (sorry, I'm retracting your "accepted answer", but at least, since you hinted at it, I feel less guilty). Commented Nov 1, 2012 at 1:51 what aboutx^2-(-x)^2 = (x-(-x))*(x+(-x)) = (x-(-x))*0 = 0$? We have: $$(-x) * x + x * x = 0 * x = 0$$ Therefore: $$-(x * x) = (-x) * x$$ Similarly: $$-(x * x) = x * (-x)$$ Apply these results to$(-x) * (-x)\$ To get what you want:

$$(-x) * (-x) = -(x * (-x)) = -(-(x * x)) = x * x$$

Another approach: The proof is easy if the ring has identity, and if not, the ring can always be embedded in a ring with identity. If the statement is true in the larger ring, it's true in the original subring.