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 𝐶 ) ) )