Metamath Proof Explorer

Theorem muls4d

Description: Rearrangement of four surreal factors. (Contributed by Scott Fenton, 16-Apr-2025)

Ref Expression
Hypotheses muls4d.1 ⊢ φ → A ∈ No
muls4d.2 ⊢ φ → B ∈ No
muls4d.3 ⊢ φ → C ∈ No
muls4d.4 ⊢ φ → D ∈ No
Assertion muls4d ⊢ φ → A ⋅ s B ⋅ s C ⋅ s D = A ⋅ s C ⋅ s B ⋅ s D

Proof

Step Hyp Ref Expression
1 muls4d.1 ⊢ φ → A ∈ No
2 muls4d.2 ⊢ φ → B ∈ No
3 muls4d.3 ⊢ φ → C ∈ No
4 muls4d.4 ⊢ φ → D ∈ No
5 2 3 mulscomd ⊢ φ → B ⋅ s C = C ⋅ s B
6 5 oveq1d ⊢ φ → B ⋅ s C ⋅ s D = C ⋅ s B ⋅ s D
7 2 3 4 mulsassd ⊢ φ → B ⋅ s C ⋅ s D = B ⋅ s C ⋅ s D
8 3 2 4 mulsassd ⊢ φ → C ⋅ s B ⋅ s D = C ⋅ s B ⋅ s D
9 6 7 8 3eqtr3d ⊢ φ → B ⋅ s C ⋅ s D = C ⋅ s B ⋅ s D
10 9 oveq2d ⊢ φ → A ⋅ s B ⋅ s C ⋅ s D = A ⋅ s C ⋅ s B ⋅ s D
11 3 4 mulscld ⊢ φ → C ⋅ s D ∈ No
12 1 2 11 mulsassd ⊢ φ → A ⋅ s B ⋅ s C ⋅ s D = A ⋅ s B ⋅ s C ⋅ s D
13 2 4 mulscld ⊢ φ → B ⋅ s D ∈ No
14 1 3 13 mulsassd ⊢ φ → A ⋅ s C ⋅ s B ⋅ s D = A ⋅ s C ⋅ s B ⋅ s D
15 10 12 14 3eqtr4d ⊢ φ → A ⋅ s B ⋅ s C ⋅ s D = A ⋅ s C ⋅ s B ⋅ s D