Metamath Proof Explorer


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 ) ) ) )