Theorem subsid

Description: Subtraction of a surreal from itself. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	subsid	$$⊢A\in \mathrm{No}\to A{-}_{s}A=0_s$$

Proof

Step	Hyp	Ref	Expression
1		subsval	$$⊢\left(A\in \mathrm{No}\wedge A\in \mathrm{No}\right)\to A{-}_{s}A=A{+}_s{+}_s\left(A\right)$$
2	1	anidms	$$⊢A\in \mathrm{No}\to A{-}_{s}A=A{+}_s{+}_s\left(A\right)$$
3		negsid	$$⊢A\in \mathrm{No}\to A{+}_s{+}_s\left(A\right)=0_s$$
4	2 3	eqtrd	$$⊢A\in \mathrm{No}\to A{-}_{s}A=0_s$$