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 ) ) )