Metamath Proof Explorer

Theorem divmuldivsd

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

Ref Expression
Hypotheses divmuldivsd.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
divmuldivsd.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
divmuldivsd.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
divmuldivsd.4 ⊢ ( 𝜑 → 𝐷 ∈ No )
divmuldivsd.5 ⊢ ( 𝜑 → 𝐵 ≠ 0s )
divmuldivsd.6 ⊢ ( 𝜑 → 𝐷 ≠ 0s )
Assertion divmuldivsd ( 𝜑 → ( ( 𝐴 /su 𝐵 ) ·s ( 𝐶 /su 𝐷 ) ) = ( ( 𝐴 ·s 𝐶 ) /su ( 𝐵 ·s 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 divmuldivsd.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
2 divmuldivsd.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
3 divmuldivsd.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
4 divmuldivsd.4 ⊢ ( 𝜑 → 𝐷 ∈ No )
5 divmuldivsd.5 ⊢ ( 𝜑 → 𝐵 ≠ 0s )
6 divmuldivsd.6 ⊢ ( 𝜑 → 𝐷 ≠ 0s )
7 1 2 5 divscld ⊢ ( 𝜑 → ( 𝐴 /su 𝐵 ) ∈ No )
8 3 4 6 divscld ⊢ ( 𝜑 → ( 𝐶 /su 𝐷 ) ∈ No )
9 2 4 7 8 muls4d ⊢ ( 𝜑 → ( ( 𝐵 ·s 𝐷 ) ·s ( ( 𝐴 /su 𝐵 ) ·s ( 𝐶 /su 𝐷 ) ) ) = ( ( 𝐵 ·s ( 𝐴 /su 𝐵 ) ) ·s ( 𝐷 ·s ( 𝐶 /su 𝐷 ) ) ) )
10 1 2 5 divscan2d ⊢ ( 𝜑 → ( 𝐵 ·s ( 𝐴 /su 𝐵 ) ) = 𝐴 )
11 3 4 6 divscan2d ⊢ ( 𝜑 → ( 𝐷 ·s ( 𝐶 /su 𝐷 ) ) = 𝐶 )
12 10 11 oveq12d ⊢ ( 𝜑 → ( ( 𝐵 ·s ( 𝐴 /su 𝐵 ) ) ·s ( 𝐷 ·s ( 𝐶 /su 𝐷 ) ) ) = ( 𝐴 ·s 𝐶 ) )
13 9 12 eqtrd ⊢ ( 𝜑 → ( ( 𝐵 ·s 𝐷 ) ·s ( ( 𝐴 /su 𝐵 ) ·s ( 𝐶 /su 𝐷 ) ) ) = ( 𝐴 ·s 𝐶 ) )
14 1 3 mulscld ⊢ ( 𝜑 → ( 𝐴 ·s 𝐶 ) ∈ No )
15 7 8 mulscld ⊢ ( 𝜑 → ( ( 𝐴 /su 𝐵 ) ·s ( 𝐶 /su 𝐷 ) ) ∈ No )
16 2 4 mulscld ⊢ ( 𝜑 → ( 𝐵 ·s 𝐷 ) ∈ No )
17 2 4 mulsne0bd ⊢ ( 𝜑 → ( ( 𝐵 ·s 𝐷 ) ≠ 0s ↔ ( 𝐵 ≠ 0s ∧ 𝐷 ≠ 0s ) ) )
18 5 6 17 mpbir2and ⊢ ( 𝜑 → ( 𝐵 ·s 𝐷 ) ≠ 0s )
19 14 15 16 18 divmulsd ⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝐶 ) /su ( 𝐵 ·s 𝐷 ) ) = ( ( 𝐴 /su 𝐵 ) ·s ( 𝐶 /su 𝐷 ) ) ↔ ( ( 𝐵 ·s 𝐷 ) ·s ( ( 𝐴 /su 𝐵 ) ·s ( 𝐶 /su 𝐷 ) ) ) = ( 𝐴 ·s 𝐶 ) ) )
20 13 19 mpbird ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐶 ) /su ( 𝐵 ·s 𝐷 ) ) = ( ( 𝐴 /su 𝐵 ) ·s ( 𝐶 /su 𝐷 ) ) )
21 20 eqcomd ⊢ ( 𝜑 → ( ( 𝐴 /su 𝐵 ) ·s ( 𝐶 /su 𝐷 ) ) = ( ( 𝐴 ·s 𝐶 ) /su ( 𝐵 ·s 𝐷 ) ) )