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\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	$$⊢L\left(A\right)\in \mathrm{V}$$
8		fvex	$$⊢R\left(A\right)\in \mathrm{V}$$
9	7 8	unex	$$⊢L\left(A\right)\cup R\left(A\right)\in \mathrm{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\to R\left(x\right)=R\left(A\right)$$
15	14	imaeq2d	$$⊢x=A\to n\left[R\left(x\right)\right]=n\left[R\left(A\right)\right]$$
16		fveq2	$$⊢x=A\to L\left(x\right)=L\left(A\right)$$
17	16	imaeq2d	$$⊢x=A\to n\left[L\left(x\right)\right]=n\left[L\left(A\right)\right]$$
18	15 17	oveq12d	$$⊢x=A\to n\left[R\left(x\right)\right]{|}_{s}n\left[L\left(x\right)\right]=n\left[R\left(A\right)\right]{|}_{s}n\left[L\left(A\right)\right]$$
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	$$⊢\left(x\in \mathrm{V},n\in \mathrm{V}⟼n\left[R\left(x\right)\right]{|}_{s}n\left[L\left(x\right)\right]\right)=\left(x\in \mathrm{V},n\in \mathrm{V}⟼n\left[R\left(x\right)\right]{|}_{s}n\left[L\left(x\right)\right]\right)$$
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\left(A\right)\subseteq L\left(A\right)\cup R\left(A\right)$$
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\left(A\right)\subseteq L\left(A\right)\cup R\left(A\right)$$
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 |-