Theorem negsval

Description: The value of the surreal negation function. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	negsval	|- ( A e. No -> ( -us ` A ) = ( ( -us " ( _R ` A ) ) |s ( -us " ( _L ` A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-negs	|- -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) )
2	1	norecov	|- ( A e. No -> ( -us ` A ) = ( A ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) ) )
3		elex	|- ( A e. No -> A e. _V )
4		negsfn	|- -us Fn No
5		fnfun	|- ( -us Fn No -> Fun -us )
6	4 5	ax-mp	|- Fun -us
7		fvex	|- ( _L ` A ) e. _V
8		fvex	|- ( _R ` A ) e. _V
9	7 8	unex	|- ( ( _L ` A ) u. ( _R ` A ) ) e. _V
10		resfunexg	|- ( ( Fun -us /\ ( ( _L ` A ) u. ( _R ` A ) ) e. _V ) -> ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) e. _V )
11	6 9 10	mp2an	|- ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) e. _V
12	11	a1i	|- ( A e. No -> ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) e. _V )
13		ovexd	|- ( A e. No -> ( ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) |s ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) ) e. _V )
14		fveq2	|- ( x = A -> ( _R ` x ) = ( _R ` A ) )
15	14	imaeq2d	|- ( x = A -> ( n " ( _R ` x ) ) = ( n " ( _R ` A ) ) )
16		fveq2	|- ( x = A -> ( _L ` x ) = ( _L ` A ) )
17	16	imaeq2d	|- ( x = A -> ( n " ( _L ` x ) ) = ( n " ( _L ` A ) ) )
18	15 17	oveq12d	|- ( x = A -> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) = ( ( n " ( _R ` A ) ) |s ( n " ( _L ` A ) ) ) )
19		imaeq1	|- ( n = ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) -> ( n " ( _R ` A ) ) = ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) )
20		imaeq1	|- ( n = ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) -> ( n " ( _L ` A ) ) = ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) )
21	19 20	oveq12d	|- ( n = ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) -> ( ( n " ( _R ` A ) ) |s ( n " ( _L ` A ) ) ) = ( ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) |s ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) ) )
22		eqid	|- ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) = ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) )
23	18 21 22	ovmpog	|- ( ( A e. _V /\ ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) e. _V /\ ( ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) |s ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) ) e. _V ) -> ( A ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) ) = ( ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) |s ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) ) )
24	3 12 13 23	syl3anc	|- ( A e. No -> ( A ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) ) = ( ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) |s ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) ) )
25		ssun2	|- ( _R ` A ) C_ ( ( _L ` A ) u. ( _R ` A ) )
26		resima2	|- ( ( _R ` A ) C_ ( ( _L ` A ) u. ( _R ` A ) ) -> ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) = ( -us " ( _R ` A ) ) )
27	25 26	ax-mp	|- ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) = ( -us " ( _R ` A ) )
28		ssun1	|- ( _L ` A ) C_ ( ( _L ` A ) u. ( _R ` A ) )
29		resima2	|- ( ( _L ` A ) C_ ( ( _L ` A ) u. ( _R ` A ) ) -> ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) = ( -us " ( _L ` A ) ) )
30	28 29	ax-mp	|- ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) = ( -us " ( _L ` A ) )
31	27 30	oveq12i	|- ( ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) |s ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) ) = ( ( -us " ( _R ` A ) ) |s ( -us " ( _L ` A ) ) )
32	31	a1i	|- ( A e. No -> ( ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) |s ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) ) = ( ( -us " ( _R ` A ) ) |s ( -us " ( _L ` A ) ) ) )
33	2 24 32	3eqtrd	|- ( A e. No -> ( -us ` A ) = ( ( -us " ( _R ` A ) ) |s ( -us " ( _L ` A ) ) ) )