Theorem negsubsdi2d

Description: Distribution of negative over subtraction. (Contributed by Scott Fenton, 5-Feb-2025)

	Ref	Expression
Hypotheses	negsubsdi2d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	negsubsdi2d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion	negsubsdi2d	⊢ ( 𝜑 → ( -us ‘ ( 𝐴 -s 𝐵 ) ) = ( 𝐵 -s 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		negsubsdi2d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		negsubsdi2d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3	2	negscld	⊢ ( 𝜑 → ( -us ‘ 𝐵 ) ∈ No )
4		negsdi	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐵 ) ∈ No ) → ( -us ‘ ( 𝐴 +s ( -us ‘ 𝐵 ) ) ) = ( ( -us ‘ 𝐴 ) +s ( -us ‘ ( -us ‘ 𝐵 ) ) ) )
5	1 3 4	syl2anc	⊢ ( 𝜑 → ( -us ‘ ( 𝐴 +s ( -us ‘ 𝐵 ) ) ) = ( ( -us ‘ 𝐴 ) +s ( -us ‘ ( -us ‘ 𝐵 ) ) ) )
6		negnegs	⊢ ( 𝐵 ∈ No → ( -us ‘ ( -us ‘ 𝐵 ) ) = 𝐵 )
7	2 6	syl	⊢ ( 𝜑 → ( -us ‘ ( -us ‘ 𝐵 ) ) = 𝐵 )
8	7	oveq2d	⊢ ( 𝜑 → ( ( -us ‘ 𝐴 ) +s ( -us ‘ ( -us ‘ 𝐵 ) ) ) = ( ( -us ‘ 𝐴 ) +s 𝐵 ) )
9	1	negscld	⊢ ( 𝜑 → ( -us ‘ 𝐴 ) ∈ No )
10	9 2	addscomd	⊢ ( 𝜑 → ( ( -us ‘ 𝐴 ) +s 𝐵 ) = ( 𝐵 +s ( -us ‘ 𝐴 ) ) )
11	5 8 10	3eqtrd	⊢ ( 𝜑 → ( -us ‘ ( 𝐴 +s ( -us ‘ 𝐵 ) ) ) = ( 𝐵 +s ( -us ‘ 𝐴 ) ) )
12	1 2	subsvald	⊢ ( 𝜑 → ( 𝐴 -s 𝐵 ) = ( 𝐴 +s ( -us ‘ 𝐵 ) ) )
13	12	fveq2d	⊢ ( 𝜑 → ( -us ‘ ( 𝐴 -s 𝐵 ) ) = ( -us ‘ ( 𝐴 +s ( -us ‘ 𝐵 ) ) ) )
14	2 1	subsvald	⊢ ( 𝜑 → ( 𝐵 -s 𝐴 ) = ( 𝐵 +s ( -us ‘ 𝐴 ) ) )
15	11 13 14	3eqtr4d	⊢ ( 𝜑 → ( -us ‘ ( 𝐴 -s 𝐵 ) ) = ( 𝐵 -s 𝐴 ) )