Theorem subsval

Description: The value of surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢x=A\to x{+}_s{+}_s\left(y\right)=A{+}_s{+}_s\left(y\right)$$
2		fveq2	$$⊢y=B\to {+}_s\left(y\right)={+}_s\left(B\right)$$
3	2	oveq2d	$$⊢y=B\to A{+}_s{+}_s\left(y\right)=A{+}_s{+}_s\left(B\right)$$
4		df-subs	$$⊢{-}_s=\left(x\in \mathrm{No},y\in \mathrm{No}⟼x{+}_s{+}_s\left(y\right)\right)$$
5		ovex	$$⊢A{+}_s{+}_s\left(B\right)\in \mathrm{V}$$
6	1 3 4 5	ovmpo	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{-}_{s}B=A{+}_s{+}_s\left(B\right)$$