Metamath Proof Explorer


Theorem subsdid

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 subsdid φ A s B - s C = A s B - s A s C

Proof

Step Hyp Ref Expression
1 addsdid.1 φ A No
2 addsdid.2 φ B No
3 addsdid.3 φ C No
4 2 3 subscld φ B - s C No
5 1 3 4 addsdid φ A s C + s B - s C = A s C + s A s B - s C
6 pncan3s C No B No C + s B - s C = B
7 3 2 6 syl2anc φ C + s B - s C = B
8 7 oveq2d φ A s C + s B - s C = A s B
9 5 8 eqtr3d φ A s C + s A s B - s C = A s B
10 1 2 mulscld φ A s B No
11 1 3 mulscld φ A s C No
12 1 4 mulscld φ A s B - s C No
13 10 11 12 subaddsd φ A s B - s A s C = A s B - s C A s C + s A s B - s C = A s B
14 9 13 mpbird φ A s B - s A s C = A s B - s C
15 14 eqcomd φ A s B - s C = A s B - s A s C