Theorem abssnid

Description: For a negative surreal, its absolute value is its negation. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Assertion	abssnid	|- ( ( A e. No /\ A <_s 0s ) -> ( abs_s ` A ) = ( -us ` A ) )

Proof

Step	Hyp	Ref	Expression
1		0sno	|- 0s e. No
2		sleloe	|- ( ( A e. No /\ 0s e. No ) -> ( A <_s 0s <-> ( A
3	1 2	mpan2	|- ( A e. No -> ( A <_s 0s <-> ( A
4		sltnle	|- ( ( A e. No /\ 0s e. No ) -> ( A -. 0s <_s A ) )
5	1 4	mpan2	|- ( A e. No -> ( A -. 0s <_s A ) )
6		abssval	|- ( A e. No -> ( abs_s ` A ) = if ( 0s <_s A , A , ( -us ` A ) ) )
7		iffalse	|- ( -. 0s <_s A -> if ( 0s <_s A , A , ( -us ` A ) ) = ( -us ` A ) )
8	6 7	sylan9eq	|- ( ( A e. No /\ -. 0s <_s A ) -> ( abs_s ` A ) = ( -us ` A ) )
9	8	ex	|- ( A e. No -> ( -. 0s <_s A -> ( abs_s ` A ) = ( -us ` A ) ) )
10	5 9	sylbid	|- ( A e. No -> ( A ( abs_s ` A ) = ( -us ` A ) ) )
11		abs0s	|- ( abs_s ` 0s ) = 0s
12		negs0s	|- ( -us ` 0s ) = 0s
13	11 12	eqtr4i	|- ( abs_s ` 0s ) = ( -us ` 0s )
14		fveq2	|- ( A = 0s -> ( abs_s ` A ) = ( abs_s ` 0s ) )
15		fveq2	|- ( A = 0s -> ( -us ` A ) = ( -us ` 0s ) )
16	13 14 15	3eqtr4a	|- ( A = 0s -> ( abs_s ` A ) = ( -us ` A ) )
17	16	a1i	|- ( A e. No -> ( A = 0s -> ( abs_s ` A ) = ( -us ` A ) ) )
18	10 17	jaod	|- ( A e. No -> ( ( A ( abs_s ` A ) = ( -us ` A ) ) )
19	3 18	sylbid	|- ( A e. No -> ( A <_s 0s -> ( abs_s ` A ) = ( -us ` A ) ) )
20	19	imp	|- ( ( A e. No /\ A <_s 0s ) -> ( abs_s ` A ) = ( -us ` A ) )