Theorem negsdi

Description: Distribution of surreal negative over addition. (Contributed by Scott Fenton, 5-Feb-2025)

	Ref	Expression
Assertion	negsdi	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to {+}_s\left(A{+}_{s}B\right)={+}_s\left(A\right){+}_s{+}_s\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		addscl	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{+}_{s}B\in \mathrm{No}$$
2	1	negsidd	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{+}_{s}B\right){+}_s{+}_s\left(A{+}_{s}B\right)=0_s$$
3		negsid	$$⊢A\in \mathrm{No}\to A{+}_s{+}_s\left(A\right)=0_s$$
4		negsid	$$⊢B\in \mathrm{No}\to B{+}_s{+}_s\left(B\right)=0_s$$
5	3 4	oveqan12d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{+}_s{+}_s\left(A\right)\right){+}_s\left(B{+}_s{+}_s\left(B\right)\right)=0_s{+}_s{0}_s$$
6		0no	$$⊢0_s\in \mathrm{No}$$
7		addslid	$$⊢0_s\in \mathrm{No}\to 0_s{+}_s{0}_s=0_s$$
8	6 7	ax-mp	$$⊢0_s{+}_s{0}_s=0_s$$
9	5 8	eqtr2di	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to 0_s=\left(A{+}_s{+}_s\left(A\right)\right){+}_s\left(B{+}_s{+}_s\left(B\right)\right)$$
10		simpl	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A\in \mathrm{No}$$
11	10	negscld	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to {+}_s\left(A\right)\in \mathrm{No}$$
12		simpr	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to B\in \mathrm{No}$$
13	12	negscld	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to {+}_s\left(B\right)\in \mathrm{No}$$
14	10 11 12 13	adds4d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{+}_s{+}_s\left(A\right)\right){+}_s\left(B{+}_s{+}_s\left(B\right)\right)=\left(A{+}_{s}B\right){+}_s\left({+}_s\left(A\right){+}_s{+}_s\left(B\right)\right)$$
15	2 9 14	3eqtrd	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{+}_{s}B\right){+}_s{+}_s\left(A{+}_{s}B\right)=\left(A{+}_{s}B\right){+}_s\left({+}_s\left(A\right){+}_s{+}_s\left(B\right)\right)$$
16	1	negscld	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to {+}_s\left(A{+}_{s}B\right)\in \mathrm{No}$$
17		negscl	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)\in \mathrm{No}$$
18		negscl	$$⊢B\in \mathrm{No}\to {+}_s\left(B\right)\in \mathrm{No}$$
19		addscl	$$⊢\left({+}_s\left(A\right)\in \mathrm{No}\wedge {+}_s\left(B\right)\in \mathrm{No}\right)\to {+}_s\left(A\right){+}_s{+}_s\left(B\right)\in \mathrm{No}$$
20	17 18 19	syl2an	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to {+}_s\left(A\right){+}_s{+}_s\left(B\right)\in \mathrm{No}$$
21	16 20 1	addscan1d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(\left(A{+}_{s}B\right){+}_s{+}_s\left(A{+}_{s}B\right)=\left(A{+}_{s}B\right){+}_s\left({+}_s\left(A\right){+}_s{+}_s\left(B\right)\right)\leftrightarrow {+}_s\left(A{+}_{s}B\right)={+}_s\left(A\right){+}_s{+}_s\left(B\right)\right)$$
22	15 21	mpbid	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to {+}_s\left(A{+}_{s}B\right)={+}_s\left(A\right){+}_s{+}_s\left(B\right)$$