Metamath Proof Explorer

Theorem divsdird

Description: Distribution of surreal division over addition. (Contributed by Scott Fenton, 13-Aug-2025)

Ref Expression
Hypotheses divsdird.1 
|- ( ph -> A e. No )
divsdird.2 
|- ( ph -> B e. No )
divsdird.3 
|- ( ph -> C e. No )
divsdird.4 
|- ( ph -> C =/= 0s )
Assertion divsdird 
|- ( ph -> ( ( A +s B ) /su C ) = ( ( A /su C ) +s ( B /su C ) ) )

Proof

Step Hyp Ref Expression
1 divsdird.1 
 |-  ( ph -> A e. No )
2 divsdird.2 
 |-  ( ph -> B e. No )
3 divsdird.3 
 |-  ( ph -> C e. No )
4 divsdird.4 
 |-  ( ph -> C =/= 0s )
5 1sno 
 |-  1s e. No
6 5 a1i 
 |-  ( ph -> 1s e. No )
7 6 3 4 divscld 
 |-  ( ph -> ( 1s /su C ) e. No )
8 1 2 7 addsdird 
 |-  ( ph -> ( ( A +s B ) x.s ( 1s /su C ) ) = ( ( A x.s ( 1s /su C ) ) +s ( B x.s ( 1s /su C ) ) ) )
9 1 2 addscld 
 |-  ( ph -> ( A +s B ) e. No )
10 9 3 4 divsrecd 
 |-  ( ph -> ( ( A +s B ) /su C ) = ( ( A +s B ) x.s ( 1s /su C ) ) )
11 1 3 4 divsrecd 
 |-  ( ph -> ( A /su C ) = ( A x.s ( 1s /su C ) ) )
12 2 3 4 divsrecd 
 |-  ( ph -> ( B /su C ) = ( B x.s ( 1s /su C ) ) )
13 11 12 oveq12d 
 |-  ( ph -> ( ( A /su C ) +s ( B /su C ) ) = ( ( A x.s ( 1s /su C ) ) +s ( B x.s ( 1s /su C ) ) ) )
14 8 10 13 3eqtr4d 
 |-  ( ph -> ( ( A +s B ) /su C ) = ( ( A /su C ) +s ( B /su C ) ) )