Theorem abssval

Description: The value of surreal absolute value. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Assertion	abssval	$$⊢A\in \mathrm{No}\to {abs}_s\left(A\right)=if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-abss	$$⊢{abs}_s=\left(x\in \mathrm{No}⟼if\left(0_s{\le }_{s}x,x,{+}_s\left(x\right)\right)\right)$$
2		breq2	$$⊢x=A\to \left(0_s{\le }_{s}x\leftrightarrow 0_s{\le }_{s}A\right)$$
3		id	$$⊢x=A\to x=A$$
4		fveq2	$$⊢x=A\to {+}_s\left(x\right)={+}_s\left(A\right)$$
5	2 3 4	ifbieq12d	$$⊢x=A\to if\left(0_s{\le }_{s}x,x,{+}_s\left(x\right)\right)=if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)$$
6		id	$$⊢A\in \mathrm{No}\to A\in \mathrm{No}$$
7		negscl	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)\in \mathrm{No}$$
8	6 7	ifcld	$$⊢A\in \mathrm{No}\to if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)\in \mathrm{No}$$
9	1 5 6 8	fvmptd3	$$⊢A\in \mathrm{No}\to {abs}_s\left(A\right)=if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)$$