Theorem divscan3d

Description: A cancellation law for surreal division. (Contributed by Scott Fenton, 13-Aug-2025)

	Ref	Expression
Hypotheses	divscan3d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	divscan3d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	divscan3d.3	⊢ ( 𝜑 → 𝐵 ≠ 0s )
Assertion	divscan3d	⊢ ( 𝜑 → ( ( 𝐵 ·s 𝐴 ) /su 𝐵 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		divscan3d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		divscan3d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		divscan3d.3	⊢ ( 𝜑 → 𝐵 ≠ 0s )
4		eqid	⊢ ( 𝐵 ·s 𝐴 ) = ( 𝐵 ·s 𝐴 )
5	2 1	mulscld	⊢ ( 𝜑 → ( 𝐵 ·s 𝐴 ) ∈ No )
6	5 1 2 3	divsmuld	⊢ ( 𝜑 → ( ( ( 𝐵 ·s 𝐴 ) /su 𝐵 ) = 𝐴 ↔ ( 𝐵 ·s 𝐴 ) = ( 𝐵 ·s 𝐴 ) ) )
7	4 6	mpbiri	⊢ ( 𝜑 → ( ( 𝐵 ·s 𝐴 ) /su 𝐵 ) = 𝐴 )