Theorem subsid

Description: Subtraction of a surreal from itself. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	subsid	⊢ ( 𝐴 ∈ No → ( 𝐴 -s 𝐴 ) = 0s )

Proof

Step	Hyp	Ref	Expression
1		subsval	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ∈ No ) → ( 𝐴 -s 𝐴 ) = ( 𝐴 +s ( -us ‘ 𝐴 ) ) )
2	1	anidms	⊢ ( 𝐴 ∈ No → ( 𝐴 -s 𝐴 ) = ( 𝐴 +s ( -us ‘ 𝐴 ) ) )
3		negsid	⊢ ( 𝐴 ∈ No → ( 𝐴 +s ( -us ‘ 𝐴 ) ) = 0s )
4	2 3	eqtrd	⊢ ( 𝐴 ∈ No → ( 𝐴 -s 𝐴 ) = 0s )