Theorem abssubs

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

	Ref	Expression
Assertion	abssubs	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( abss ‘ ( 𝐴 -s 𝐵 ) ) = ( abss ‘ ( 𝐵 -s 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐵 ∈ No )
2		simpl	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐴 ∈ No )
3	1 2	negsubsdi2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( -us ‘ ( 𝐵 -s 𝐴 ) ) = ( 𝐴 -s 𝐵 ) )
4	3	fveq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( abss ‘ ( -us ‘ ( 𝐵 -s 𝐴 ) ) ) = ( abss ‘ ( 𝐴 -s 𝐵 ) ) )
5		subscl	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( 𝐵 -s 𝐴 ) ∈ No )
6	5	ancoms	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐵 -s 𝐴 ) ∈ No )
7		absnegs	⊢ ( ( 𝐵 -s 𝐴 ) ∈ No → ( abss ‘ ( -us ‘ ( 𝐵 -s 𝐴 ) ) ) = ( abss ‘ ( 𝐵 -s 𝐴 ) ) )
8	6 7	syl	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( abss ‘ ( -us ‘ ( 𝐵 -s 𝐴 ) ) ) = ( abss ‘ ( 𝐵 -s 𝐴 ) ) )
9	4 8	eqtr3d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( abss ‘ ( 𝐴 -s 𝐵 ) ) = ( abss ‘ ( 𝐵 -s 𝐴 ) ) )