Metamath Proof Explorer

Theorem divmuldivsd

Description: Multiplication of two surreal ratios. (Contributed by Scott Fenton, 16-Apr-2025)

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

Proof

Step Hyp Ref Expression
1 divmuldivsd.1 
 |-  ( ph -> A e. No )
2 divmuldivsd.2 
 |-  ( ph -> B e. No )
3 divmuldivsd.3 
 |-  ( ph -> C e. No )
4 divmuldivsd.4 
 |-  ( ph -> D e. No )
5 divmuldivsd.5 
 |-  ( ph -> B =/= 0s )
6 divmuldivsd.6 
 |-  ( ph -> D =/= 0s )
7 1 2 5 divscld 
 |-  ( ph -> ( A /su B ) e. No )
8 3 4 6 divscld 
 |-  ( ph -> ( C /su D ) e. No )
9 2 4 7 8 muls4d 
 |-  ( ph -> ( ( B x.s D ) x.s ( ( A /su B ) x.s ( C /su D ) ) ) = ( ( B x.s ( A /su B ) ) x.s ( D x.s ( C /su D ) ) ) )
10 1 2 5 divscan2d 
 |-  ( ph -> ( B x.s ( A /su B ) ) = A )
11 3 4 6 divscan2d 
 |-  ( ph -> ( D x.s ( C /su D ) ) = C )
12 10 11 oveq12d 
 |-  ( ph -> ( ( B x.s ( A /su B ) ) x.s ( D x.s ( C /su D ) ) ) = ( A x.s C ) )
13 9 12 eqtrd 
 |-  ( ph -> ( ( B x.s D ) x.s ( ( A /su B ) x.s ( C /su D ) ) ) = ( A x.s C ) )
14 1 3 mulscld 
 |-  ( ph -> ( A x.s C ) e. No )
15 7 8 mulscld 
 |-  ( ph -> ( ( A /su B ) x.s ( C /su D ) ) e. No )
16 2 4 mulscld 
 |-  ( ph -> ( B x.s D ) e. No )
17 2 4 mulsne0bd 
 |-  ( ph -> ( ( B x.s D ) =/= 0s <-> ( B =/= 0s /\ D =/= 0s ) ) )
18 5 6 17 mpbir2and 
 |-  ( ph -> ( B x.s D ) =/= 0s )
19 14 15 16 18 divsmuld 
 |-  ( ph -> ( ( ( A x.s C ) /su ( B x.s D ) ) = ( ( A /su B ) x.s ( C /su D ) ) <-> ( ( B x.s D ) x.s ( ( A /su B ) x.s ( C /su D ) ) ) = ( A x.s C ) ) )
20 13 19 mpbird 
 |-  ( ph -> ( ( A x.s C ) /su ( B x.s D ) ) = ( ( A /su B ) x.s ( C /su D ) ) )
21 20 eqcomd 
 |-  ( ph -> ( ( A /su B ) x.s ( C /su D ) ) = ( ( A x.s C ) /su ( B x.s D ) ) )