Theorem muls4d

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

	Ref	Expression
Hypotheses	muls4d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	muls4d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	muls4d.3	⊢ ( 𝜑 → 𝐶 ∈ No )
	muls4d.4	⊢ ( 𝜑 → 𝐷 ∈ No )
Assertion	muls4d	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) ·s ( 𝐶 ·s 𝐷 ) ) = ( ( 𝐴 ·s 𝐶 ) ·s ( 𝐵 ·s 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		muls4d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		muls4d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		muls4d.3	⊢ ( 𝜑 → 𝐶 ∈ No )
4		muls4d.4	⊢ ( 𝜑 → 𝐷 ∈ No )
5	2 3	mulscomd	⊢ ( 𝜑 → ( 𝐵 ·s 𝐶 ) = ( 𝐶 ·s 𝐵 ) )
6	5	oveq1d	⊢ ( 𝜑 → ( ( 𝐵 ·s 𝐶 ) ·s 𝐷 ) = ( ( 𝐶 ·s 𝐵 ) ·s 𝐷 ) )
7	2 3 4	mulsassd	⊢ ( 𝜑 → ( ( 𝐵 ·s 𝐶 ) ·s 𝐷 ) = ( 𝐵 ·s ( 𝐶 ·s 𝐷 ) ) )
8	3 2 4	mulsassd	⊢ ( 𝜑 → ( ( 𝐶 ·s 𝐵 ) ·s 𝐷 ) = ( 𝐶 ·s ( 𝐵 ·s 𝐷 ) ) )
9	6 7 8	3eqtr3d	⊢ ( 𝜑 → ( 𝐵 ·s ( 𝐶 ·s 𝐷 ) ) = ( 𝐶 ·s ( 𝐵 ·s 𝐷 ) ) )
10	9	oveq2d	⊢ ( 𝜑 → ( 𝐴 ·s ( 𝐵 ·s ( 𝐶 ·s 𝐷 ) ) ) = ( 𝐴 ·s ( 𝐶 ·s ( 𝐵 ·s 𝐷 ) ) ) )
11	3 4	mulscld	⊢ ( 𝜑 → ( 𝐶 ·s 𝐷 ) ∈ No )
12	1 2 11	mulsassd	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) ·s ( 𝐶 ·s 𝐷 ) ) = ( 𝐴 ·s ( 𝐵 ·s ( 𝐶 ·s 𝐷 ) ) ) )
13	2 4	mulscld	⊢ ( 𝜑 → ( 𝐵 ·s 𝐷 ) ∈ No )
14	1 3 13	mulsassd	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐶 ) ·s ( 𝐵 ·s 𝐷 ) ) = ( 𝐴 ·s ( 𝐶 ·s ( 𝐵 ·s 𝐷 ) ) ) )
15	10 12 14	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) ·s ( 𝐶 ·s 𝐷 ) ) = ( ( 𝐴 ·s 𝐶 ) ·s ( 𝐵 ·s 𝐷 ) ) )