Theorem lt2addsd

Description: Adding both sides of two surreal less-than relations. (Contributed by Scott Fenton, 15-Apr-2025)

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

Proof

Step	Hyp	Ref	Expression
1		lt2addsd.1	$$⊢\phi \to A\in \mathrm{No}$$
2		lt2addsd.2	$$⊢\phi \to B\in \mathrm{No}$$
3		lt2addsd.3	$$⊢\phi \to C\in \mathrm{No}$$
4		lt2addsd.4	$$⊢\phi \to D\in \mathrm{No}$$
5		lt2addsd.5	$$⊢\phi \to A{<}_{s}C$$
6		lt2addsd.6	$$⊢\phi \to B{<}_{s}D$$
7	1 2	addscld	$$⊢\phi \to A{+}_{s}B\in \mathrm{No}$$
8	3 2	addscld	$$⊢\phi \to C{+}_{s}B\in \mathrm{No}$$
9	3 4	addscld	$$⊢\phi \to C{+}_{s}D\in \mathrm{No}$$
10	1 3 2	ltadds1d	$$⊢\phi \to \left(A{<}_{s}C\leftrightarrow \left(A{+}_{s}B\right){<}_s\left(C{+}_{s}B\right)\right)$$
11	5 10	mpbid	$$⊢\phi \to \left(A{+}_{s}B\right){<}_s\left(C{+}_{s}B\right)$$
12	2 4 3	ltadds2d	$$⊢\phi \to \left(B{<}_{s}D\leftrightarrow \left(C{+}_{s}B\right){<}_s\left(C{+}_{s}D\right)\right)$$
13	6 12	mpbid	$$⊢\phi \to \left(C{+}_{s}B\right){<}_s\left(C{+}_{s}D\right)$$
14	7 8 9 11 13	ltstrd	$$⊢\phi \to \left(A{+}_{s}B\right){<}_s\left(C{+}_{s}D\right)$$