Theorem mul2negsd

Description: Surreal product of two negatives. (Contributed by Scott Fenton, 15-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		mulnegs1d.1	$$⊢\phi \to A\in \mathrm{No}$$
2		mulnegs1d.2	$$⊢\phi \to B\in \mathrm{No}$$
3	2	negscld	$$⊢\phi \to {+}_s\left(B\right)\in \mathrm{No}$$
4	1 3	mulnegs1d	$$⊢\phi \to {+}_s\left(A\right){\cdot }_s{+}_s\left(B\right)={+}_s\left(A{\cdot }_s{+}_s\left(B\right)\right)$$
5	1 2	mulnegs2d	$$⊢\phi \to A{\cdot }_s{+}_s\left(B\right)={+}_s\left(A{\cdot }_{s}B\right)$$
6	5	fveq2d	$$⊢\phi \to {+}_s\left(A{\cdot }_s{+}_s\left(B\right)\right)={+}_s\left({+}_s\left(A{\cdot }_{s}B\right)\right)$$
7	1 2	mulscld	$$⊢\phi \to A{\cdot }_{s}B\in \mathrm{No}$$
8		negnegs	$$⊢A{\cdot }_{s}B\in \mathrm{No}\to {+}_s\left({+}_s\left(A{\cdot }_{s}B\right)\right)=A{\cdot }_{s}B$$
9	7 8	syl	$$⊢\phi \to {+}_s\left({+}_s\left(A{\cdot }_{s}B\right)\right)=A{\cdot }_{s}B$$
10	4 6 9	3eqtrd	$$⊢\phi \to {+}_s\left(A\right){\cdot }_s{+}_s\left(B\right)=A{\cdot }_{s}B$$