Metamath Proof Explorer


Theorem subsdird

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

Ref Expression
Hypotheses addsdid.1 φ A No
addsdid.2 φ B No
addsdid.3 φ C No
Assertion subsdird φ A - s B s C = A s C - s B s C

Proof

Step Hyp Ref Expression
1 addsdid.1 φ A No
2 addsdid.2 φ B No
3 addsdid.3 φ C No
4 3 1 2 subsdid φ C s A - s B = C s A - s C s B
5 1 2 subscld φ A - s B No
6 5 3 mulscomd φ A - s B s C = C s A - s B
7 1 3 mulscomd φ A s C = C s A
8 2 3 mulscomd φ B s C = C s B
9 7 8 oveq12d φ A s C - s B s C = C s A - s C s B
10 4 6 9 3eqtr4d φ A - s B s C = A s C - s B s C