Metamath Proof Explorer


Theorem negsval

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

Ref Expression
Assertion negsval Could not format assertion : No typesetting found for |- ( A e. No -> ( -us ` A ) = ( ( -us " ( _R ` A ) ) |s ( -us " ( _L ` A ) ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 df-negs Could not format -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) ) : No typesetting found for |- -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) ) with typecode |-
2 1 norecov Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
3 elex A No A V
4 negsfn Could not format -us Fn No : No typesetting found for |- -us Fn No with typecode |-
5 fnfun Could not format ( -us Fn No -> Fun -us ) : No typesetting found for |- ( -us Fn No -> Fun -us ) with typecode |-
6 4 5 ax-mp Could not format Fun -us : No typesetting found for |- Fun -us with typecode |-
7 fvex L A V
8 fvex R A V
9 7 8 unex L A R A V
10 resfunexg Could not format ( ( Fun -us /\ ( ( _L ` A ) u. ( _R ` A ) ) e. _V ) -> ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) e. _V ) : No typesetting found for |- ( ( Fun -us /\ ( ( _L ` A ) u. ( _R ` A ) ) e. _V ) -> ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) e. _V ) with typecode |-
11 6 9 10 mp2an Could not format ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) e. _V : No typesetting found for |- ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) e. _V with typecode |-
12 11 a1i Could not format ( A e. No -> ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) e. _V ) : No typesetting found for |- ( A e. No -> ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) e. _V ) with typecode |-
13 ovexd Could not format ( A e. No -> ( ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) |s ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) ) e. _V ) : No typesetting found for |- ( A e. No -> ( ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) |s ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) ) e. _V ) with typecode |-
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 Could not format ( n = ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) -> ( n " ( _R ` A ) ) = ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) ) : No typesetting found for |- ( n = ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) -> ( n " ( _R ` A ) ) = ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) ) with typecode |-
20 imaeq1 Could not format ( n = ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) -> ( n " ( _L ` A ) ) = ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) ) : No typesetting found for |- ( n = ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) -> ( n " ( _L ` A ) ) = ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) ) with typecode |-
21 19 20 oveq12d Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
22 eqid x V , n V n R x | s n L x = x V , n V n R x | s n L x
23 18 21 22 ovmpog Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
24 3 12 13 23 syl3anc Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
25 ssun2 R A L A R A
26 resima2 Could not format ( ( _R ` A ) C_ ( ( _L ` A ) u. ( _R ` A ) ) -> ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) = ( -us " ( _R ` A ) ) ) : No typesetting found for |- ( ( _R ` A ) C_ ( ( _L ` A ) u. ( _R ` A ) ) -> ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) = ( -us " ( _R ` A ) ) ) with typecode |-
27 25 26 ax-mp Could not format ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) = ( -us " ( _R ` A ) ) : No typesetting found for |- ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) = ( -us " ( _R ` A ) ) with typecode |-
28 ssun1 L A L A R A
29 resima2 Could not format ( ( _L ` A ) C_ ( ( _L ` A ) u. ( _R ` A ) ) -> ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) = ( -us " ( _L ` A ) ) ) : No typesetting found for |- ( ( _L ` A ) C_ ( ( _L ` A ) u. ( _R ` A ) ) -> ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) = ( -us " ( _L ` A ) ) ) with typecode |-
30 28 29 ax-mp Could not format ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) = ( -us " ( _L ` A ) ) : No typesetting found for |- ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) = ( -us " ( _L ` A ) ) with typecode |-
31 27 30 oveq12i Could not format ( ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) |s ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) ) = ( ( -us " ( _R ` A ) ) |s ( -us " ( _L ` A ) ) ) : No typesetting found for |- ( ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _R ` A ) ) |s ( ( -us |` ( ( _L ` A ) u. ( _R ` A ) ) ) " ( _L ` A ) ) ) = ( ( -us " ( _R ` A ) ) |s ( -us " ( _L ` A ) ) ) with typecode |-
32 31 a1i Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
33 2 24 32 3eqtrd Could not format ( A e. No -> ( -us ` A ) = ( ( -us " ( _R ` A ) ) |s ( -us " ( _L ` A ) ) ) ) : No typesetting found for |- ( A e. No -> ( -us ` A ) = ( ( -us " ( _R ` A ) ) |s ( -us " ( _L ` A ) ) ) ) with typecode |-