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 ⊢ φ → A ∈ No
divsasswd.2 ⊢ φ → B ∈ No
divsasswd.3 ⊢ φ → C ∈ No
divsasswd.4 ⊢ φ → C ≠ 0 s
divsasswd.5 ⊢ φ → ∃ x ∈ No C ⋅ s x = 1 s
Assertion divsasswd ⊢ φ → A ⋅ s B / su C = A ⋅ s B / su C

Proof

Step Hyp Ref Expression
1 divsasswd.1 ⊢ φ → A ∈ No
2 divsasswd.2 ⊢ φ → B ∈ No
3 divsasswd.3 ⊢ φ → C ∈ No
4 divsasswd.4 ⊢ φ → C ≠ 0 s
5 divsasswd.5 ⊢ φ → ∃ x ∈ No C ⋅ s x = 1 s
6 2 3 4 5 divscan2wd ⊢ φ → C ⋅ s B / su C = B
7 6 oveq2d ⊢ φ → A ⋅ s C ⋅ s B / su C = A ⋅ s B
8 2 3 4 5 divsclwd ⊢ φ → B / su C ∈ No
9 3 1 8 muls12d ⊢ φ → C ⋅ s A ⋅ s B / su C = A ⋅ s C ⋅ s B / su C
10 1 2 mulscld ⊢ φ → A ⋅ s B ∈ No
11 10 3 4 5 divscan2wd ⊢ φ → C ⋅ s A ⋅ s B / su C = A ⋅ s B
12 7 9 11 3eqtr4rd ⊢ φ → C ⋅ s A ⋅ s B / su C = C ⋅ s A ⋅ s B / su C
13 10 3 4 5 divsclwd ⊢ φ → A ⋅ s B / su C ∈ No
14 1 8 mulscld ⊢ φ → A ⋅ s B / su C ∈ No
15 13 14 3 4 mulscan1d ⊢ φ → C ⋅ s A ⋅ s B / su C = C ⋅ s A ⋅ s B / su C ↔ A ⋅ s B / su C = A ⋅ s B / su C
16 12 15 mpbid ⊢ φ → A ⋅ s B / su C = A ⋅ s B / su C