Theorem negsval2

Description: Surreal negation in terms of subtraction. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	negsval2	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)=0_s{-}_{s}A$$

Proof

Step	Hyp	Ref	Expression
1		0sno	$$⊢0_s\in \mathrm{No}$$
2		subsval	$$⊢\left(0_s\in \mathrm{No}\wedge A\in \mathrm{No}\right)\to 0_s{-}_{s}A=0_s{+}_s{+}_s\left(A\right)$$
3	1 2	mpan	$$⊢A\in \mathrm{No}\to 0_s{-}_{s}A=0_s{+}_s{+}_s\left(A\right)$$
4		negscl	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)\in \mathrm{No}$$
5		addslid	$$⊢{+}_s\left(A\right)\in \mathrm{No}\to 0_s{+}_s{+}_s\left(A\right)={+}_s\left(A\right)$$
6	4 5	syl	$$⊢A\in \mathrm{No}\to 0_s{+}_s{+}_s\left(A\right)={+}_s\left(A\right)$$
7	3 6	eqtr2d	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)=0_s{-}_{s}A$$