Theorem subsubs4d

Description: Law for double surreal subtraction. (Contributed by Scott Fenton, 9-Mar-2025)

	Ref	Expression
Hypotheses	subsubs4d.1	$$⊢\phi \to A\in \mathrm{No}$$
	subsubs4d.2	$$⊢\phi \to B\in \mathrm{No}$$
	subsubs4d.3	$$⊢\phi \to C\in \mathrm{No}$$
Assertion	subsubs4d	$$⊢\phi \to \left(A{-}_{s}B\right){-}_{s}C=A{-}_s\left(B{+}_{s}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		subsubs4d.1	$$⊢\phi \to A\in \mathrm{No}$$
2		subsubs4d.2	$$⊢\phi \to B\in \mathrm{No}$$
3		subsubs4d.3	$$⊢\phi \to C\in \mathrm{No}$$
4	2	negscld	$$⊢\phi \to {+}_s\left(B\right)\in \mathrm{No}$$
5	3	negscld	$$⊢\phi \to {+}_s\left(C\right)\in \mathrm{No}$$
6	1 4 5	addsassd	$$⊢\phi \to \left(A{+}_s{+}_s\left(B\right)\right){+}_s{+}_s\left(C\right)=A{+}_s\left({+}_s\left(B\right){+}_s{+}_s\left(C\right)\right)$$
7	1 2	subsvald	$$⊢\phi \to A{-}_{s}B=A{+}_s{+}_s\left(B\right)$$
8	7	oveq1d	$$⊢\phi \to \left(A{-}_{s}B\right){-}_{s}C=\left(A{+}_s{+}_s\left(B\right)\right){-}_{s}C$$
9	1 4	addscld	$$⊢\phi \to A{+}_s{+}_s\left(B\right)\in \mathrm{No}$$
10	9 3	subsvald	$$⊢\phi \to \left(A{+}_s{+}_s\left(B\right)\right){-}_{s}C=\left(A{+}_s{+}_s\left(B\right)\right){+}_s{+}_s\left(C\right)$$
11	8 10	eqtrd	$$⊢\phi \to \left(A{-}_{s}B\right){-}_{s}C=\left(A{+}_s{+}_s\left(B\right)\right){+}_s{+}_s\left(C\right)$$
12	2 3	addscld	$$⊢\phi \to B{+}_{s}C\in \mathrm{No}$$
13	1 12	subsvald	$$⊢\phi \to A{-}_s\left(B{+}_{s}C\right)=A{+}_s{+}_s\left(B{+}_{s}C\right)$$
14		negsdi	$$⊢\left(B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to {+}_s\left(B{+}_{s}C\right)={+}_s\left(B\right){+}_s{+}_s\left(C\right)$$
15	2 3 14	syl2anc	$$⊢\phi \to {+}_s\left(B{+}_{s}C\right)={+}_s\left(B\right){+}_s{+}_s\left(C\right)$$
16	15	oveq2d	$$⊢\phi \to A{+}_s{+}_s\left(B{+}_{s}C\right)=A{+}_s\left({+}_s\left(B\right){+}_s{+}_s\left(C\right)\right)$$
17	13 16	eqtrd	$$⊢\phi \to A{-}_s\left(B{+}_{s}C\right)=A{+}_s\left({+}_s\left(B\right){+}_s{+}_s\left(C\right)\right)$$
18	6 11 17	3eqtr4d	$$⊢\phi \to \left(A{-}_{s}B\right){-}_{s}C=A{-}_s\left(B{+}_{s}C\right)$$