Theorem divscan3d

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

	Ref	Expression
Hypotheses	divscan3d.1	|- ( ph -> A e. No )
	divscan3d.2	|- ( ph -> B e. No )
	divscan3d.3	|- ( ph -> B =/= 0s )
Assertion	divscan3d	|- ( ph -> ( ( B x.s A ) /su B ) = A )

Proof

Step	Hyp	Ref	Expression
1		divscan3d.1	|- ( ph -> A e. No )
2		divscan3d.2	|- ( ph -> B e. No )
3		divscan3d.3	|- ( ph -> B =/= 0s )
4		eqid	|- ( B x.s A ) = ( B x.s A )
5	2 1	mulscld	|- ( ph -> ( B x.s A ) e. No )
6	5 1 2 3	divsmuld	|- ( ph -> ( ( ( B x.s A ) /su B ) = A <-> ( B x.s A ) = ( B x.s A ) ) )
7	4 6	mpbiri	|- ( ph -> ( ( B x.s A ) /su B ) = A )