Metamath Proof Explorer


Theorem addsdird

Description: Distributive law for surreal numbers. Part of theorem 7 of Conway p. 19. (Contributed by Scott Fenton, 9-Mar-2025)

Ref Expression
Hypotheses addsdid.1 φ A No
addsdid.2 φ B No
addsdid.3 φ C No
Assertion addsdird φ 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 addsdid φ C s A + s B = C s A + s C s B
5 1 2 addscld φ 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