Theorem negnegs

Description: A surreal is equal to the negative of its negative. Theorem 4(ii) of Conway p. 17. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	negnegs	$$⊢A\in \mathrm{No}\to {+}_s\left({+}_s\left(A\right)\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		negscl	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)\in \mathrm{No}$$
2	1	negsidd	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right){+}_s{+}_s\left({+}_s\left(A\right)\right)=0_s$$
3	1	negscld	$$⊢A\in \mathrm{No}\to {+}_s\left({+}_s\left(A\right)\right)\in \mathrm{No}$$
4	3 1	addscomd	$$⊢A\in \mathrm{No}\to {+}_s\left({+}_s\left(A\right)\right){+}_s{+}_s\left(A\right)={+}_s\left(A\right){+}_s{+}_s\left({+}_s\left(A\right)\right)$$
5		negsid	$$⊢A\in \mathrm{No}\to A{+}_s{+}_s\left(A\right)=0_s$$
6	2 4 5	3eqtr4d	$$⊢A\in \mathrm{No}\to {+}_s\left({+}_s\left(A\right)\right){+}_s{+}_s\left(A\right)=A{+}_s{+}_s\left(A\right)$$
7		id	$$⊢A\in \mathrm{No}\to A\in \mathrm{No}$$
8	3 7 1	addscan2d	$$⊢A\in \mathrm{No}\to \left({+}_s\left({+}_s\left(A\right)\right){+}_s{+}_s\left(A\right)=A{+}_s{+}_s\left(A\right)\leftrightarrow {+}_s\left({+}_s\left(A\right)\right)=A\right)$$
9	6 8	mpbid	$$⊢A\in \mathrm{No}\to {+}_s\left({+}_s\left(A\right)\right)=A$$