Metamath Proof Explorer


Theorem dvmptsub

Description: Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses dvmptadd.s φS
dvmptadd.a φxXA
dvmptadd.b φxXBV
dvmptadd.da φdxXAdSx=xXB
dvmptsub.c φxXC
dvmptsub.d φxXDW
dvmptsub.dc φdxXCdSx=xXD
Assertion dvmptsub φdxXACdSx=xXBD

Proof

Step Hyp Ref Expression
1 dvmptadd.s φS
2 dvmptadd.a φxXA
3 dvmptadd.b φxXBV
4 dvmptadd.da φdxXAdSx=xXB
5 dvmptsub.c φxXC
6 dvmptsub.d φxXDW
7 dvmptsub.dc φdxXCdSx=xXD
8 5 negcld φxXC
9 negex DV
10 9 a1i φxXDV
11 1 5 6 7 dvmptneg φdxXCdSx=xXD
12 1 2 3 4 8 10 11 dvmptadd φdxXA+CdSx=xXB+D
13 2 5 negsubd φxXA+C=AC
14 13 mpteq2dva φxXA+C=xXAC
15 14 oveq2d φdxXA+CdSx=dxXACdSx
16 1 2 3 4 dvmptcl φxXB
17 1 5 6 7 dvmptcl φxXD
18 16 17 negsubd φxXB+D=BD
19 18 mpteq2dva φxXB+D=xXBD
20 12 15 19 3eqtr3d φdxXACdSx=xXBD