Metamath Proof Explorer

Theorem negsfv

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

Ref Expression
Assertion negsfv 
|- ( 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 ) ) ) )