Theorem subscan1d

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

	Ref	Expression
Hypotheses	subscand.1	$$⊢\phi \to A\in \mathrm{No}$$
	subscand.2	$$⊢\phi \to B\in \mathrm{No}$$
	subscand.3	$$⊢\phi \to C\in \mathrm{No}$$
Assertion	subscan1d	$$⊢\phi \to \left(C{-}_{s}A=C{-}_{s}B\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		subscand.1	$$⊢\phi \to A\in \mathrm{No}$$
2		subscand.2	$$⊢\phi \to B\in \mathrm{No}$$
3		subscand.3	$$⊢\phi \to C\in \mathrm{No}$$
4	3 1	subsvald	$$⊢\phi \to C{-}_{s}A=C{+}_s{+}_s\left(A\right)$$
5	3 2	subsvald	$$⊢\phi \to C{-}_{s}B=C{+}_s{+}_s\left(B\right)$$
6	4 5	eqeq12d	$$⊢\phi \to \left(C{-}_{s}A=C{-}_{s}B\leftrightarrow C{+}_s{+}_s\left(A\right)=C{+}_s{+}_s\left(B\right)\right)$$
7	1	negscld	$$⊢\phi \to {+}_s\left(A\right)\in \mathrm{No}$$
8	2	negscld	$$⊢\phi \to {+}_s\left(B\right)\in \mathrm{No}$$
9	7 8 3	addscan1d	$$⊢\phi \to \left(C{+}_s{+}_s\left(A\right)=C{+}_s{+}_s\left(B\right)\leftrightarrow {+}_s\left(A\right)={+}_s\left(B\right)\right)$$
10		negs11	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left({+}_s\left(A\right)={+}_s\left(B\right)\leftrightarrow A=B\right)$$
11	1 2 10	syl2anc	$$⊢\phi \to \left({+}_s\left(A\right)={+}_s\left(B\right)\leftrightarrow A=B\right)$$
12	6 9 11	3bitrd	$$⊢\phi \to \left(C{-}_{s}A=C{-}_{s}B\leftrightarrow A=B\right)$$