Theorem subscan1d

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	subscan1d	|- ( ph -> ( ( C -s A ) = ( C -s B ) <-> 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	3 1	subsvald	|- ( ph -> ( C -s A ) = ( C +s ( -us ` A ) ) )
5	3 2	subsvald	|- ( ph -> ( C -s B ) = ( C +s ( -us ` B ) ) )
6	4 5	eqeq12d	|- ( ph -> ( ( C -s A ) = ( C -s B ) <-> ( C +s ( -us ` A ) ) = ( C +s ( -us ` B ) ) ) )
7	1	negscld	|- ( ph -> ( -us ` A ) e. No )
8	2	negscld	|- ( ph -> ( -us ` B ) e. No )
9	7 8 3	addscan1d	|- ( ph -> ( ( C +s ( -us ` A ) ) = ( C +s ( -us ` B ) ) <-> ( -us ` A ) = ( -us ` B ) ) )
10		negs11	|- ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) = ( -us ` B ) <-> A = B ) )
11	1 2 10	syl2anc	|- ( ph -> ( ( -us ` A ) = ( -us ` B ) <-> A = B ) )
12	6 9 11	3bitrd	|- ( ph -> ( ( C -s A ) = ( C -s B ) <-> A = B ) )