Theorem absssub

Description: Swapping order of surreal subtraction doesn't change the absolute value. (Contributed by Scott Fenton, 29-Jan-2026)

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

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to B\in \mathrm{No}$$
2		simpl	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A\in \mathrm{No}$$
3	1 2	negsubsdi2d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to {+}_s\left(B{-}_{s}A\right)=A{-}_{s}B$$
4	3	fveq2d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to {abs}_s\left({+}_s\left(B{-}_{s}A\right)\right)={abs}_s\left(A{-}_{s}B\right)$$
5		subscl	$$⊢\left(B\in \mathrm{No}\wedge A\in \mathrm{No}\right)\to B{-}_{s}A\in \mathrm{No}$$
6	5	ancoms	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to B{-}_{s}A\in \mathrm{No}$$
7		abssneg	$$⊢B{-}_{s}A\in \mathrm{No}\to {abs}_s\left({+}_s\left(B{-}_{s}A\right)\right)={abs}_s\left(B{-}_{s}A\right)$$
8	6 7	syl	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to {abs}_s\left({+}_s\left(B{-}_{s}A\right)\right)={abs}_s\left(B{-}_{s}A\right)$$
9	4 8	eqtr3d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to {abs}_s\left(A{-}_{s}B\right)={abs}_s\left(B{-}_{s}A\right)$$