Theorem subscan1d

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

	Ref	Expression
Hypotheses	subscand.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	subscand.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	subscand.3	⊢ ( 𝜑 → 𝐶 ∈ No )
Assertion	subscan1d	⊢ ( 𝜑 → ( ( 𝐶 -s 𝐴 ) = ( 𝐶 -s 𝐵 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		subscand.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		subscand.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		subscand.3	⊢ ( 𝜑 → 𝐶 ∈ No )
4	3 1	subsvald	⊢ ( 𝜑 → ( 𝐶 -s 𝐴 ) = ( 𝐶 +s ( -us ‘ 𝐴 ) ) )
5	3 2	subsvald	⊢ ( 𝜑 → ( 𝐶 -s 𝐵 ) = ( 𝐶 +s ( -us ‘ 𝐵 ) ) )
6	4 5	eqeq12d	⊢ ( 𝜑 → ( ( 𝐶 -s 𝐴 ) = ( 𝐶 -s 𝐵 ) ↔ ( 𝐶 +s ( -us ‘ 𝐴 ) ) = ( 𝐶 +s ( -us ‘ 𝐵 ) ) ) )
7	1	negscld	⊢ ( 𝜑 → ( -us ‘ 𝐴 ) ∈ No )
8	2	negscld	⊢ ( 𝜑 → ( -us ‘ 𝐵 ) ∈ No )
9	7 8 3	addscan1d	⊢ ( 𝜑 → ( ( 𝐶 +s ( -us ‘ 𝐴 ) ) = ( 𝐶 +s ( -us ‘ 𝐵 ) ) ↔ ( -us ‘ 𝐴 ) = ( -us ‘ 𝐵 ) ) )
10		negs11	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( -us ‘ 𝐴 ) = ( -us ‘ 𝐵 ) ↔ 𝐴 = 𝐵 ) )
11	1 2 10	syl2anc	⊢ ( 𝜑 → ( ( -us ‘ 𝐴 ) = ( -us ‘ 𝐵 ) ↔ 𝐴 = 𝐵 ) )
12	6 9 11	3bitrd	⊢ ( 𝜑 → ( ( 𝐶 -s 𝐴 ) = ( 𝐶 -s 𝐵 ) ↔ 𝐴 = 𝐵 ) )