Theorem subscan2d

Description: Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Hypotheses	subscand.1	|- ( ph -> A e. No )
	subscand.2	|- ( ph -> B e. No )
	subscand.3	|- ( ph -> C e. No )
Assertion	subscan2d	|- ( ph -> ( ( A -s C ) = ( B -s C ) <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		subscand.1	|- ( ph -> A e. No )
2		subscand.2	|- ( ph -> B e. No )
3		subscand.3	|- ( ph -> C e. No )
4	1 3	subsvald	|- ( ph -> ( A -s C ) = ( A +s ( -us ` C ) ) )
5	2 3	subsvald	|- ( ph -> ( B -s C ) = ( B +s ( -us ` C ) ) )
6	4 5	eqeq12d	|- ( ph -> ( ( A -s C ) = ( B -s C ) <-> ( A +s ( -us ` C ) ) = ( B +s ( -us ` C ) ) ) )
7	3	negscld	|- ( ph -> ( -us ` C ) e. No )
8	1 2 7	addscan2d	|- ( ph -> ( ( A +s ( -us ` C ) ) = ( B +s ( -us ` C ) ) <-> A = B ) )
9	6 8	bitrd	|- ( ph -> ( ( A -s C ) = ( B -s C ) <-> A = B ) )