Metamath Proof Explorer

Theorem muls4d

Description: Rearrangement of four surreal factors. (Contributed by Scott Fenton, 16-Apr-2025)

Ref Expression
Hypotheses muls4d.1 
|- ( ph -> A e. No )
muls4d.2 
|- ( ph -> B e. No )
muls4d.3 
|- ( ph -> C e. No )
muls4d.4 
|- ( ph -> D e. No )
Assertion muls4d 
|- ( ph -> ( ( A x.s B ) x.s ( C x.s D ) ) = ( ( A x.s C ) x.s ( B x.s D ) ) )

Proof

Step Hyp Ref Expression
1 muls4d.1 
 |-  ( ph -> A e. No )
2 muls4d.2 
 |-  ( ph -> B e. No )
3 muls4d.3 
 |-  ( ph -> C e. No )
4 muls4d.4 
 |-  ( ph -> D e. No )
5 2 3 mulscomd 
 |-  ( ph -> ( B x.s C ) = ( C x.s B ) )
6 5 oveq1d 
 |-  ( ph -> ( ( B x.s C ) x.s D ) = ( ( C x.s B ) x.s D ) )
7 2 3 4 mulsassd 
 |-  ( ph -> ( ( B x.s C ) x.s D ) = ( B x.s ( C x.s D ) ) )
8 3 2 4 mulsassd 
 |-  ( ph -> ( ( C x.s B ) x.s D ) = ( C x.s ( B x.s D ) ) )
9 6 7 8 3eqtr3d 
 |-  ( ph -> ( B x.s ( C x.s D ) ) = ( C x.s ( B x.s D ) ) )
10 9 oveq2d 
 |-  ( ph -> ( A x.s ( B x.s ( C x.s D ) ) ) = ( A x.s ( C x.s ( B x.s D ) ) ) )
11 3 4 mulscld 
 |-  ( ph -> ( C x.s D ) e. No )
12 1 2 11 mulsassd 
 |-  ( ph -> ( ( A x.s B ) x.s ( C x.s D ) ) = ( A x.s ( B x.s ( C x.s D ) ) ) )
13 2 4 mulscld 
 |-  ( ph -> ( B x.s D ) e. No )
14 1 3 13 mulsassd 
 |-  ( ph -> ( ( A x.s C ) x.s ( B x.s D ) ) = ( A x.s ( C x.s ( B x.s D ) ) ) )
15 10 12 14 3eqtr4d 
 |-  ( ph -> ( ( A x.s B ) x.s ( C x.s D ) ) = ( ( A x.s C ) x.s ( B x.s D ) ) )