Theorem subscan2d

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	subscan2d	⊢ ( 𝜑 → ( ( 𝐴 -s 𝐶 ) = ( 𝐵 -s 𝐶 ) ↔ 𝐴 = 𝐵 ) )

Proof

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