Theorem neg0s

Description: Negative surreal zero is surreal zero. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	neg0s	$$⊢{+}_s\left(0_s\right)=0_s$$

Proof

Step	Hyp	Ref	Expression
1		right0s	$$⊢R\left(0_s\right)=\varnothing$$
2	1	imaeq2i	$$⊢{+}_s\left[R\left(0_s\right)\right]={+}_s\left[\varnothing \right]$$
3		ima0	$$⊢{+}_s\left[\varnothing \right]=\varnothing$$
4	2 3	eqtri	$$⊢{+}_s\left[R\left(0_s\right)\right]=\varnothing$$
5		left0s	$$⊢L\left(0_s\right)=\varnothing$$
6	5	imaeq2i	$$⊢{+}_s\left[L\left(0_s\right)\right]={+}_s\left[\varnothing \right]$$
7	6 3	eqtri	$$⊢{+}_s\left[L\left(0_s\right)\right]=\varnothing$$
8	4 7	oveq12i	$$⊢{+}_s\left[R\left(0_s\right)\right]{|}_s{+}_s\left[L\left(0_s\right)\right]=\varnothing {|}_s\varnothing$$
9		0no	$$⊢0_s\in \mathrm{No}$$
10		negsval	$$⊢0_s\in \mathrm{No}\to {+}_s\left(0_s\right)={+}_s\left[R\left(0_s\right)\right]{|}_s{+}_s\left[L\left(0_s\right)\right]$$
11	9 10	ax-mp	$$⊢{+}_s\left(0_s\right)={+}_s\left[R\left(0_s\right)\right]{|}_s{+}_s\left[L\left(0_s\right)\right]$$
12		df-0s	$$⊢0_s=\varnothing {|}_s\varnothing$$
13	8 11 12	3eqtr4i	$$⊢{+}_s\left(0_s\right)=0_s$$