Theorem abssneg

Description: Surreal absolute value of the negative. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Assertion	abssneg	|- ( A e. No -> ( abs_s ` ( -us ` A ) ) = ( abs_s ` A ) )

Proof

Step	Hyp	Ref	Expression
1		negnegs	|- ( A e. No -> ( -us ` ( -us ` A ) ) = A )
2	1	adantr	|- ( ( A e. No /\ 0s <_s A ) -> ( -us ` ( -us ` A ) ) = A )
3		negscl	|- ( A e. No -> ( -us ` A ) e. No )
4		0sno	|- 0s e. No
5	4	a1i	|- ( A e. No -> 0s e. No )
6		id	|- ( A e. No -> A e. No )
7	5 6	slenegd	|- ( A e. No -> ( 0s <_s A <-> ( -us ` A ) <_s ( -us ` 0s ) ) )
8		negs0s	|- ( -us ` 0s ) = 0s
9	8	breq2i	|- ( ( -us ` A ) <_s ( -us ` 0s ) <-> ( -us ` A ) <_s 0s )
10	7 9	bitrdi	|- ( A e. No -> ( 0s <_s A <-> ( -us ` A ) <_s 0s ) )
11	10	biimpa	|- ( ( A e. No /\ 0s <_s A ) -> ( -us ` A ) <_s 0s )
12		abssnid	|- ( ( ( -us ` A ) e. No /\ ( -us ` A ) <_s 0s ) -> ( abs_s ` ( -us ` A ) ) = ( -us ` ( -us ` A ) ) )
13	3 11 12	syl2an2r	|- ( ( A e. No /\ 0s <_s A ) -> ( abs_s ` ( -us ` A ) ) = ( -us ` ( -us ` A ) ) )
14		abssid	|- ( ( A e. No /\ 0s <_s A ) -> ( abs_s ` A ) = A )
15	2 13 14	3eqtr4d	|- ( ( A e. No /\ 0s <_s A ) -> ( abs_s ` ( -us ` A ) ) = ( abs_s ` A ) )
16	6 5	slenegd	|- ( A e. No -> ( A <_s 0s <-> ( -us ` 0s ) <_s ( -us ` A ) ) )
17	8	breq1i	|- ( ( -us ` 0s ) <_s ( -us ` A ) <-> 0s <_s ( -us ` A ) )
18	16 17	bitrdi	|- ( A e. No -> ( A <_s 0s <-> 0s <_s ( -us ` A ) ) )
19	18	biimpa	|- ( ( A e. No /\ A <_s 0s ) -> 0s <_s ( -us ` A ) )
20		abssid	|- ( ( ( -us ` A ) e. No /\ 0s <_s ( -us ` A ) ) -> ( abs_s ` ( -us ` A ) ) = ( -us ` A ) )
21	3 19 20	syl2an2r	|- ( ( A e. No /\ A <_s 0s ) -> ( abs_s ` ( -us ` A ) ) = ( -us ` A ) )
22		abssnid	|- ( ( A e. No /\ A <_s 0s ) -> ( abs_s ` A ) = ( -us ` A ) )
23	21 22	eqtr4d	|- ( ( A e. No /\ A <_s 0s ) -> ( abs_s ` ( -us ` A ) ) = ( abs_s ` A ) )
24		sletric	|- ( ( 0s e. No /\ A e. No ) -> ( 0s <_s A \/ A <_s 0s ) )
25	4 24	mpan	|- ( A e. No -> ( 0s <_s A \/ A <_s 0s ) )
26	15 23 25	mpjaodan	|- ( A e. No -> ( abs_s ` ( -us ` A ) ) = ( abs_s ` A ) )