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 ⊢ ( 𝜑 → 𝐴 ∈ No )
divsasswd.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
divsasswd.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
divsasswd.4 ⊢ ( 𝜑 → 𝐶 ≠ 0s )
divsasswd.5 ⊢ ( 𝜑 → ∃ 𝑥 ∈ No ( 𝐶 ·s 𝑥 ) = 1s )
Assertion divsasswd ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) /su 𝐶 ) = ( 𝐴 ·s ( 𝐵 /su 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 divsasswd.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
2 divsasswd.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
3 divsasswd.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
4 divsasswd.4 ⊢ ( 𝜑 → 𝐶 ≠ 0s )
5 divsasswd.5 ⊢ ( 𝜑 → ∃ 𝑥 ∈ No ( 𝐶 ·s 𝑥 ) = 1s )
6 2 3 4 5 divscan2wd ⊢ ( 𝜑 → ( 𝐶 ·s ( 𝐵 /su 𝐶 ) ) = 𝐵 )
7 6 oveq2d ⊢ ( 𝜑 → ( 𝐴 ·s ( 𝐶 ·s ( 𝐵 /su 𝐶 ) ) ) = ( 𝐴 ·s 𝐵 ) )
8 2 3 4 5 divsclwd ⊢ ( 𝜑 → ( 𝐵 /su 𝐶 ) ∈ No )
9 3 1 8 muls12d ⊢ ( 𝜑 → ( 𝐶 ·s ( 𝐴 ·s ( 𝐵 /su 𝐶 ) ) ) = ( 𝐴 ·s ( 𝐶 ·s ( 𝐵 /su 𝐶 ) ) ) )
10 1 2 mulscld ⊢ ( 𝜑 → ( 𝐴 ·s 𝐵 ) ∈ No )
11 10 3 4 5 divscan2wd ⊢ ( 𝜑 → ( 𝐶 ·s ( ( 𝐴 ·s 𝐵 ) /su 𝐶 ) ) = ( 𝐴 ·s 𝐵 ) )
12 7 9 11 3eqtr4rd ⊢ ( 𝜑 → ( 𝐶 ·s ( ( 𝐴 ·s 𝐵 ) /su 𝐶 ) ) = ( 𝐶 ·s ( 𝐴 ·s ( 𝐵 /su 𝐶 ) ) ) )
13 10 3 4 5 divsclwd ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) /su 𝐶 ) ∈ No )
14 1 8 mulscld ⊢ ( 𝜑 → ( 𝐴 ·s ( 𝐵 /su 𝐶 ) ) ∈ No )
15 13 14 3 4 mulscan1d ⊢ ( 𝜑 → ( ( 𝐶 ·s ( ( 𝐴 ·s 𝐵 ) /su 𝐶 ) ) = ( 𝐶 ·s ( 𝐴 ·s ( 𝐵 /su 𝐶 ) ) ) ↔ ( ( 𝐴 ·s 𝐵 ) /su 𝐶 ) = ( 𝐴 ·s ( 𝐵 /su 𝐶 ) ) ) )
16 12 15 mpbid ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) /su 𝐶 ) = ( 𝐴 ·s ( 𝐵 /su 𝐶 ) ) )