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	|- ( ( A e. No /\ B e. No ) -> ( abs_s ` ( A -s B ) ) = ( abs_s ` ( B -s A ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( A e. No /\ B e. No ) -> B e. No )
2		simpl	|- ( ( A e. No /\ B e. No ) -> A e. No )
3	1 2	negsubsdi2d	|- ( ( A e. No /\ B e. No ) -> ( -us ` ( B -s A ) ) = ( A -s B ) )
4	3	fveq2d	|- ( ( A e. No /\ B e. No ) -> ( abs_s ` ( -us ` ( B -s A ) ) ) = ( abs_s ` ( A -s B ) ) )
5		subscl	|- ( ( B e. No /\ A e. No ) -> ( B -s A ) e. No )
6	5	ancoms	|- ( ( A e. No /\ B e. No ) -> ( B -s A ) e. No )
7		abssneg	|- ( ( B -s A ) e. No -> ( abs_s ` ( -us ` ( B -s A ) ) ) = ( abs_s ` ( B -s A ) ) )
8	6 7	syl	|- ( ( A e. No /\ B e. No ) -> ( abs_s ` ( -us ` ( B -s A ) ) ) = ( abs_s ` ( B -s A ) ) )
9	4 8	eqtr3d	|- ( ( A e. No /\ B e. No ) -> ( abs_s ` ( A -s B ) ) = ( abs_s ` ( B -s A ) ) )