Metamath Proof Explorer

Theorem divsasswd

Description: An associative law for surreal division. Weak version. (Contributed by Scott Fenton, 14-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 divsasswd.1 
 |-  ( ph -> A e. No )
2 divsasswd.2 
 |-  ( ph -> B e. No )
3 divsasswd.3 
 |-  ( ph -> C e. No )
4 divsasswd.4 
 |-  ( ph -> C =/= 0s )
5 divsasswd.5 
 |-  ( ph -> E. x e. No ( C x.s x ) = 1s )
6 2 3 4 5 divscan2wd 
 |-  ( ph -> ( C x.s ( B /su C ) ) = B )
7 6 oveq2d 
 |-  ( ph -> ( A x.s ( C x.s ( B /su C ) ) ) = ( A x.s B ) )
8 2 3 4 5 divsclwd 
 |-  ( ph -> ( B /su C ) e. No )
9 3 1 8 muls12d 
 |-  ( ph -> ( C x.s ( A x.s ( B /su C ) ) ) = ( A x.s ( C x.s ( B /su C ) ) ) )
10 1 2 mulscld 
 |-  ( ph -> ( A x.s B ) e. No )
11 10 3 4 5 divscan2wd 
 |-  ( ph -> ( C x.s ( ( A x.s B ) /su C ) ) = ( A x.s B ) )
12 7 9 11 3eqtr4rd 
 |-  ( ph -> ( C x.s ( ( A x.s B ) /su C ) ) = ( C x.s ( A x.s ( B /su C ) ) ) )
13 10 3 4 5 divsclwd 
 |-  ( ph -> ( ( A x.s B ) /su C ) e. No )
14 1 8 mulscld 
 |-  ( ph -> ( A x.s ( B /su C ) ) e. No )
15 13 14 3 4 mulscan1d 
 |-  ( ph -> ( ( C x.s ( ( A x.s B ) /su C ) ) = ( C x.s ( A x.s ( B /su C ) ) ) <-> ( ( A x.s B ) /su C ) = ( A x.s ( B /su C ) ) ) )
16 12 15 mpbid 
 |-  ( ph -> ( ( A x.s B ) /su C ) = ( A x.s ( B /su C ) ) )