Theorem negsval

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

	Ref	Expression
Assertion	negsval	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)={+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]$$

Proof

Step	Hyp	Ref	Expression
1		df-negs	$$⊢{+}_s={norec}_s\#A\#\left(\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)\right)$$
2	1	norecov	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)=A\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({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)$$
3		elex	$$⊢A\in \mathrm{No}\to A\in \mathrm{V}$$
4		negsfn	$$⊢{+}_{s}Fn\mathrm{No}$$
5		fnfun	$$⊢{+}_{s}Fn\mathrm{No}\to \mathrm{Fun}{+}_s$$
6	4 5	ax-mp	$$⊢\mathrm{Fun}{+}_s$$
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	$$⊢\left(\mathrm{Fun}{+}_s\wedge L\left(A\right)\cup R\left(A\right)\in \mathrm{V}\right)\to {{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\in \mathrm{V}$$
11	6 9 10	mp2an	$$⊢{{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\in \mathrm{V}$$
12	11	a1i	$$⊢A\in \mathrm{No}\to {{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\in \mathrm{V}$$
13		ovexd	$$⊢A\in \mathrm{No}\to \left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[R\left(A\right)\right]{|}_s\left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[L\left(A\right)\right]\in \mathrm{V}$$
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	$$⊢n={{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\to n\left[R\left(A\right)\right]=\left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[R\left(A\right)\right]$$
20		imaeq1	$$⊢n={{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\to n\left[L\left(A\right)\right]=\left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[L\left(A\right)\right]$$
21	19 20	oveq12d	$$⊢n={{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\to n\left[R\left(A\right)\right]{|}_{s}n\left[L\left(A\right)\right]=\left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[R\left(A\right)\right]{|}_s\left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[L\left(A\right)\right]$$
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	$$⊢\left(A\in \mathrm{V}\wedge {{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\in \mathrm{V}\wedge \left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[R\left(A\right)\right]{|}_s\left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[L\left(A\right)\right]\in \mathrm{V}\right)\to A\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({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)=\left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[R\left(A\right)\right]{|}_s\left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[L\left(A\right)\right]$$
24	3 12 13 23	syl3anc	$$⊢A\in \mathrm{No}\to A\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({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)=\left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[R\left(A\right)\right]{|}_s\left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[L\left(A\right)\right]$$
25		ssun2	$$⊢R\left(A\right)\subseteq L\left(A\right)\cup R\left(A\right)$$
26		resima2	$$⊢R\left(A\right)\subseteq L\left(A\right)\cup R\left(A\right)\to \left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[R\left(A\right)\right]={+}_s\left[R\left(A\right)\right]$$
27	25 26	ax-mp	$$⊢\left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[R\left(A\right)\right]={+}_s\left[R\left(A\right)\right]$$
28		ssun1	$$⊢L\left(A\right)\subseteq L\left(A\right)\cup R\left(A\right)$$
29		resima2	$$⊢L\left(A\right)\subseteq L\left(A\right)\cup R\left(A\right)\to \left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[L\left(A\right)\right]={+}_s\left[L\left(A\right)\right]$$
30	28 29	ax-mp	$$⊢\left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[L\left(A\right)\right]={+}_s\left[L\left(A\right)\right]$$
31	27 30	oveq12i	$$⊢\left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[R\left(A\right)\right]{|}_s\left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[L\left(A\right)\right]={+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]$$
32	31	a1i	$$⊢A\in \mathrm{No}\to \left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[R\left(A\right)\right]{|}_s\left({{+}_s\upharpoonright }_{\left(L\left(A\right)\cup R\left(A\right)\right)}\right)\left[L\left(A\right)\right]={+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]$$
33	2 24 32	3eqtrd	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)={+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]$$