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 " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-negs	Could not format -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) ) : No typesetting found for |- -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) ) with typecode |-
2	1	norecov	Could not format ( A e. No -> ( -us ` A ) = ( A ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) ) : No typesetting found for |- ( A e. No -> ( -us ` A ) = ( A ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) ) with typecode |-
3		elex	$$⊢A\in \mathrm{No}\to A\in \mathrm{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	Could not format ( _Left ` A ) e. _V : No typesetting found for |- ( _Left ` A ) e. _V with typecode |-
8		fvex	Could not format ( _Right ` A ) e. _V : No typesetting found for |- ( _Right ` A ) e. _V with typecode |-
9	7 8	unex	Could not format ( ( _Left ` A ) u. ( _Right ` A ) ) e. _V : No typesetting found for |- ( ( _Left ` A ) u. ( _Right ` A ) ) e. _V with typecode |-
10		resfunexg	Could not format ( ( Fun -us /\ ( ( _Left ` A ) u. ( _Right ` A ) ) e. _V ) -> ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) e. _V ) : No typesetting found for |- ( ( Fun -us /\ ( ( _Left ` A ) u. ( _Right ` A ) ) e. _V ) -> ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) e. _V ) with typecode |-
11	6 9 10	mp2an	Could not format ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) e. _V : No typesetting found for |- ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) e. _V with typecode |-
12	11	a1i	Could not format ( A e. No -> ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) e. _V ) : No typesetting found for |- ( A e. No -> ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) e. _V ) with typecode |-
13		ovexd	Could not format ( A e. No -> ( ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) |s ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) e. _V ) : No typesetting found for |- ( A e. No -> ( ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) |s ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) e. _V ) with typecode |-
14		fveq2	Could not format ( x = A -> ( _Right ` x ) = ( _Right ` A ) ) : No typesetting found for |- ( x = A -> ( _Right ` x ) = ( _Right ` A ) ) with typecode |-
15	14	imaeq2d	Could not format ( x = A -> ( n " ( _Right ` x ) ) = ( n " ( _Right ` A ) ) ) : No typesetting found for |- ( x = A -> ( n " ( _Right ` x ) ) = ( n " ( _Right ` A ) ) ) with typecode |-
16		fveq2	Could not format ( x = A -> ( _Left ` x ) = ( _Left ` A ) ) : No typesetting found for |- ( x = A -> ( _Left ` x ) = ( _Left ` A ) ) with typecode |-
17	16	imaeq2d	Could not format ( x = A -> ( n " ( _Left ` x ) ) = ( n " ( _Left ` A ) ) ) : No typesetting found for |- ( x = A -> ( n " ( _Left ` x ) ) = ( n " ( _Left ` A ) ) ) with typecode |-
18	15 17	oveq12d	Could not format ( x = A -> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) = ( ( n " ( _Right ` A ) ) |s ( n " ( _Left ` A ) ) ) ) : No typesetting found for |- ( x = A -> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) = ( ( n " ( _Right ` A ) ) |s ( n " ( _Left ` A ) ) ) ) with typecode |-
19		imaeq1	Could not format ( n = ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) -> ( n " ( _Right ` A ) ) = ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) ) : No typesetting found for |- ( n = ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) -> ( n " ( _Right ` A ) ) = ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) ) with typecode |-
20		imaeq1	Could not format ( n = ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) -> ( n " ( _Left ` A ) ) = ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) : No typesetting found for |- ( n = ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) -> ( n " ( _Left ` A ) ) = ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) with typecode |-
21	19 20	oveq12d	Could not format ( n = ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) -> ( ( n " ( _Right ` A ) ) |s ( n " ( _Left ` A ) ) ) = ( ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) |s ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) ) : No typesetting found for |- ( n = ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) -> ( ( n " ( _Right ` A ) ) |s ( n " ( _Left ` A ) ) ) = ( ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) |s ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) ) with typecode |-
22		eqid	Could not format ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) = ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) : No typesetting found for |- ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) = ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) with typecode |-
23	18 21 22	ovmpog	Could not format ( ( A e. _V /\ ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) e. _V /\ ( ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) |s ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) e. _V ) -> ( A ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) = ( ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) |s ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) ) : No typesetting found for |- ( ( A e. _V /\ ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) e. _V /\ ( ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) |s ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) e. _V ) -> ( A ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) = ( ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) |s ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) ) with typecode |-
24	3 12 13 23	syl3anc	Could not format ( A e. No -> ( A ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) = ( ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) |s ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) ) : No typesetting found for |- ( A e. No -> ( A ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) = ( ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) |s ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) ) with typecode |-
25		ssun2	Could not format ( _Right ` A ) C_ ( ( _Left ` A ) u. ( _Right ` A ) ) : No typesetting found for |- ( _Right ` A ) C_ ( ( _Left ` A ) u. ( _Right ` A ) ) with typecode |-
26		resima2	Could not format ( ( _Right ` A ) C_ ( ( _Left ` A ) u. ( _Right ` A ) ) -> ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) = ( -us " ( _Right ` A ) ) ) : No typesetting found for |- ( ( _Right ` A ) C_ ( ( _Left ` A ) u. ( _Right ` A ) ) -> ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) = ( -us " ( _Right ` A ) ) ) with typecode |-
27	25 26	ax-mp	Could not format ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) = ( -us " ( _Right ` A ) ) : No typesetting found for |- ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) = ( -us " ( _Right ` A ) ) with typecode |-
28		ssun1	Could not format ( _Left ` A ) C_ ( ( _Left ` A ) u. ( _Right ` A ) ) : No typesetting found for |- ( _Left ` A ) C_ ( ( _Left ` A ) u. ( _Right ` A ) ) with typecode |-
29		resima2	Could not format ( ( _Left ` A ) C_ ( ( _Left ` A ) u. ( _Right ` A ) ) -> ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) = ( -us " ( _Left ` A ) ) ) : No typesetting found for |- ( ( _Left ` A ) C_ ( ( _Left ` A ) u. ( _Right ` A ) ) -> ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) = ( -us " ( _Left ` A ) ) ) with typecode |-
30	28 29	ax-mp	Could not format ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) = ( -us " ( _Left ` A ) ) : No typesetting found for |- ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) = ( -us " ( _Left ` A ) ) with typecode |-
31	27 30	oveq12i	Could not format ( ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) |s ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) : No typesetting found for |- ( ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) |s ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) with typecode |-
32	31	a1i	Could not format ( A e. No -> ( ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) |s ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) ) : No typesetting found for |- ( A e. No -> ( ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Right ` A ) ) |s ( ( -us |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) " ( _Left ` A ) ) ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) ) with typecode |-
33	2 24 32	3eqtrd	Could not format ( A e. No -> ( -us ` A ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) ) : No typesetting found for |- ( A e. No -> ( -us ` A ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) ) with typecode |-