subsdid

Description: Distribution of surreal multiplication over subtraction. (Contributed by Scott Fenton, 9-Mar-2025)

	Ref	Expression
Hypotheses	addsdid.1	$⊢ φ \to A \in No$
	addsdid.2	$⊢ φ \to B \in No$
	addsdid.3	$⊢ φ \to C \in No$
Assertion	subsdid	$⊢ φ \to A \cdot_{s} (B -_{s} C) = (A \cdot_{s} B) -_{s} (A \cdot_{s} C)$

Step	Hyp	Ref	Expression
1		addsdid.1	$⊢ φ \to A \in No$
2		addsdid.2	$⊢ φ \to B \in No$
3		addsdid.3	$⊢ φ \to C \in No$
4	2 3	subscld	$⊢ φ \to B -_{s} C \in No$
5	1 3 4	addsdid	$⊢ φ \to A \cdot_{s} (C +_{s} (B -_{s} C)) = (A \cdot_{s} C) +_{s} (A \cdot_{s} (B -_{s} C))$
6		pncan3s	$⊢ (C \in No \land B \in No) \to C +_{s} (B -_{s} C) = B$
7	3 2 6	syl2anc	$⊢ φ \to C +_{s} (B -_{s} C) = B$
8	7	oveq2d	$⊢ φ \to A \cdot_{s} (C +_{s} (B -_{s} C)) = A \cdot_{s} B$
9	5 8	eqtr3d	$⊢ φ \to (A \cdot_{s} C) +_{s} (A \cdot_{s} (B -_{s} C)) = A \cdot_{s} B$
10	1 2	mulscld	$⊢ φ \to A \cdot_{s} B \in No$
11	1 3	mulscld	$⊢ φ \to A \cdot_{s} C \in No$
12	1 4	mulscld	$⊢ φ \to A \cdot_{s} (B -_{s} C) \in No$
13	10 11 12	subaddsd	$⊢ φ \to ((A \cdot_{s} B) -_{s} (A \cdot_{s} C) = A \cdot_{s} (B -_{s} C) \leftrightarrow (A \cdot_{s} C) +_{s} (A \cdot_{s} (B -_{s} C)) = A \cdot_{s} B)$
14	9 13	mpbird	$⊢ φ \to (A \cdot_{s} B) -_{s} (A \cdot_{s} C) = A \cdot_{s} (B -_{s} C)$
15	14	eqcomd	$⊢ φ \to A \cdot_{s} (B -_{s} C) = (A \cdot_{s} B) -_{s} (A \cdot_{s} C)$

Metamath Proof Explorer