Theorem ltsubsubsbd

Description: Equivalence for the surreal less-than relationship between differences. (Contributed by Scott Fenton, 6-Feb-2025)

	Ref	Expression
Hypotheses	ltsubsubsbd.1	$$⊢\phi \to A\in \mathrm{No}$$
	ltsubsubsbd.2	$$⊢\phi \to B\in \mathrm{No}$$
	ltsubsubsbd.3	$$⊢\phi \to C\in \mathrm{No}$$
	ltsubsubsbd.4	$$⊢\phi \to D\in \mathrm{No}$$
Assertion	ltsubsubsbd	$$⊢\phi \to \left(\left(A{-}_{s}C\right){<}_s\left(B{-}_{s}D\right)\leftrightarrow \left(A{-}_{s}B\right){<}_s\left(C{-}_{s}D\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ltsubsubsbd.1	$$⊢\phi \to A\in \mathrm{No}$$
2		ltsubsubsbd.2	$$⊢\phi \to B\in \mathrm{No}$$
3		ltsubsubsbd.3	$$⊢\phi \to C\in \mathrm{No}$$
4		ltsubsubsbd.4	$$⊢\phi \to D\in \mathrm{No}$$
5		npcans	$$⊢\left(A\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to \left(A{-}_{s}C\right){+}_{s}C=A$$
6	1 3 5	syl2anc	$$⊢\phi \to \left(A{-}_{s}C\right){+}_{s}C=A$$
7		npcans	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{-}_{s}B\right){+}_{s}B=A$$
8	1 2 7	syl2anc	$$⊢\phi \to \left(A{-}_{s}B\right){+}_{s}B=A$$
9	6 8	eqtr4d	$$⊢\phi \to \left(A{-}_{s}C\right){+}_{s}C=\left(A{-}_{s}B\right){+}_{s}B$$
10	2 3	addscomd	$$⊢\phi \to B{+}_{s}C=C{+}_{s}B$$
11	10	oveq1d	$$⊢\phi \to \left(B{+}_{s}C\right){+}_s{+}_s\left(D\right)=\left(C{+}_{s}B\right){+}_s{+}_s\left(D\right)$$
12	2 4	subsvald	$$⊢\phi \to B{-}_{s}D=B{+}_s{+}_s\left(D\right)$$
13	12	oveq1d	$$⊢\phi \to \left(B{-}_{s}D\right){+}_{s}C=\left(B{+}_s{+}_s\left(D\right)\right){+}_{s}C$$
14	4	negscld	$$⊢\phi \to {+}_s\left(D\right)\in \mathrm{No}$$
15	2 14 3	adds32d	$$⊢\phi \to \left(B{+}_s{+}_s\left(D\right)\right){+}_{s}C=\left(B{+}_{s}C\right){+}_s{+}_s\left(D\right)$$
16	13 15	eqtrd	$$⊢\phi \to \left(B{-}_{s}D\right){+}_{s}C=\left(B{+}_{s}C\right){+}_s{+}_s\left(D\right)$$
17	3 4	subsvald	$$⊢\phi \to C{-}_{s}D=C{+}_s{+}_s\left(D\right)$$
18	17	oveq1d	$$⊢\phi \to \left(C{-}_{s}D\right){+}_{s}B=\left(C{+}_s{+}_s\left(D\right)\right){+}_{s}B$$
19	3 14 2	adds32d	$$⊢\phi \to \left(C{+}_s{+}_s\left(D\right)\right){+}_{s}B=\left(C{+}_{s}B\right){+}_s{+}_s\left(D\right)$$
20	18 19	eqtrd	$$⊢\phi \to \left(C{-}_{s}D\right){+}_{s}B=\left(C{+}_{s}B\right){+}_s{+}_s\left(D\right)$$
21	11 16 20	3eqtr4d	$$⊢\phi \to \left(B{-}_{s}D\right){+}_{s}C=\left(C{-}_{s}D\right){+}_{s}B$$
22	9 21	breq12d	$$⊢\phi \to \left(\left(\left(A{-}_{s}C\right){+}_{s}C\right){<}_s\left(\left(B{-}_{s}D\right){+}_{s}C\right)\leftrightarrow \left(\left(A{-}_{s}B\right){+}_{s}B\right){<}_s\left(\left(C{-}_{s}D\right){+}_{s}B\right)\right)$$
23	1 3	subscld	$$⊢\phi \to A{-}_{s}C\in \mathrm{No}$$
24	2 4	subscld	$$⊢\phi \to B{-}_{s}D\in \mathrm{No}$$
25	23 24 3	ltadds1d	$$⊢\phi \to \left(\left(A{-}_{s}C\right){<}_s\left(B{-}_{s}D\right)\leftrightarrow \left(\left(A{-}_{s}C\right){+}_{s}C\right){<}_s\left(\left(B{-}_{s}D\right){+}_{s}C\right)\right)$$
26	1 2	subscld	$$⊢\phi \to A{-}_{s}B\in \mathrm{No}$$
27	3 4	subscld	$$⊢\phi \to C{-}_{s}D\in \mathrm{No}$$
28	26 27 2	ltadds1d	$$⊢\phi \to \left(\left(A{-}_{s}B\right){<}_s\left(C{-}_{s}D\right)\leftrightarrow \left(\left(A{-}_{s}B\right){+}_{s}B\right){<}_s\left(\left(C{-}_{s}D\right){+}_{s}B\right)\right)$$
29	22 25 28	3bitr4d	$$⊢\phi \to \left(\left(A{-}_{s}C\right){<}_s\left(B{-}_{s}D\right)\leftrightarrow \left(A{-}_{s}B\right){<}_s\left(C{-}_{s}D\right)\right)$$