Theorem negsubsdi2d

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

	Ref	Expression
Hypotheses	negsubsdi2d.1	$$⊢\phi \to A\in \mathrm{No}$$
	negsubsdi2d.2	$$⊢\phi \to B\in \mathrm{No}$$
Assertion	negsubsdi2d	Could not format assertion : No typesetting found for |- ( ph -> ( -us ` ( A -s B ) ) = ( B -s A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		negsubsdi2d.1	$$⊢\phi \to A\in \mathrm{No}$$
2		negsubsdi2d.2	$$⊢\phi \to B\in \mathrm{No}$$
3	2	negscld	Could not format ( ph -> ( -us ` B ) e. No ) : No typesetting found for |- ( ph -> ( -us ` B ) e. No ) with typecode |-
4		negsdi	Could not format ( ( A e. No /\ ( -us ` B ) e. No ) -> ( -us ` ( A +s ( -us ` B ) ) ) = ( ( -us ` A ) +s ( -us ` ( -us ` B ) ) ) ) : No typesetting found for |- ( ( A e. No /\ ( -us ` B ) e. No ) -> ( -us ` ( A +s ( -us ` B ) ) ) = ( ( -us ` A ) +s ( -us ` ( -us ` B ) ) ) ) with typecode |-
5	1 3 4	syl2anc	Could not format ( ph -> ( -us ` ( A +s ( -us ` B ) ) ) = ( ( -us ` A ) +s ( -us ` ( -us ` B ) ) ) ) : No typesetting found for |- ( ph -> ( -us ` ( A +s ( -us ` B ) ) ) = ( ( -us ` A ) +s ( -us ` ( -us ` B ) ) ) ) with typecode |-
6		negnegs	Could not format ( B e. No -> ( -us ` ( -us ` B ) ) = B ) : No typesetting found for |- ( B e. No -> ( -us ` ( -us ` B ) ) = B ) with typecode |-
7	2 6	syl	Could not format ( ph -> ( -us ` ( -us ` B ) ) = B ) : No typesetting found for |- ( ph -> ( -us ` ( -us ` B ) ) = B ) with typecode |-
8	7	oveq2d	Could not format ( ph -> ( ( -us ` A ) +s ( -us ` ( -us ` B ) ) ) = ( ( -us ` A ) +s B ) ) : No typesetting found for |- ( ph -> ( ( -us ` A ) +s ( -us ` ( -us ` B ) ) ) = ( ( -us ` A ) +s B ) ) with typecode |-
9	1	negscld	Could not format ( ph -> ( -us ` A ) e. No ) : No typesetting found for |- ( ph -> ( -us ` A ) e. No ) with typecode |-
10	9 2	addscomd	Could not format ( ph -> ( ( -us ` A ) +s B ) = ( B +s ( -us ` A ) ) ) : No typesetting found for |- ( ph -> ( ( -us ` A ) +s B ) = ( B +s ( -us ` A ) ) ) with typecode |-
11	5 8 10	3eqtrd	Could not format ( ph -> ( -us ` ( A +s ( -us ` B ) ) ) = ( B +s ( -us ` A ) ) ) : No typesetting found for |- ( ph -> ( -us ` ( A +s ( -us ` B ) ) ) = ( B +s ( -us ` A ) ) ) with typecode |-
12	1 2	subsvald	Could not format ( ph -> ( A -s B ) = ( A +s ( -us ` B ) ) ) : No typesetting found for |- ( ph -> ( A -s B ) = ( A +s ( -us ` B ) ) ) with typecode |-
13	12	fveq2d	Could not format ( ph -> ( -us ` ( A -s B ) ) = ( -us ` ( A +s ( -us ` B ) ) ) ) : No typesetting found for |- ( ph -> ( -us ` ( A -s B ) ) = ( -us ` ( A +s ( -us ` B ) ) ) ) with typecode |-
14	2 1	subsvald	Could not format ( ph -> ( B -s A ) = ( B +s ( -us ` A ) ) ) : No typesetting found for |- ( ph -> ( B -s A ) = ( B +s ( -us ` A ) ) ) with typecode |-
15	11 13 14	3eqtr4d	Could not format ( ph -> ( -us ` ( A -s B ) ) = ( B -s A ) ) : No typesetting found for |- ( ph -> ( -us ` ( A -s B ) ) = ( B -s A ) ) with typecode |-