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 ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvmptadd.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
dvmptadd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
dvmptadd.da ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
dvmptsub.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
dvmptsub.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ 𝑊 )
dvmptsub.dc ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
Assertion dvmptsub ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 − 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 − 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 dvmptadd.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvmptadd.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
3 dvmptadd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
4 dvmptadd.da ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
5 dvmptsub.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
6 dvmptsub.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ 𝑊 )
7 dvmptsub.dc ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
8 5 negcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → - 𝐶 ∈ ℂ )
9 negex ⊢ - 𝐷 ∈ V
10 9 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → - 𝐷 ∈ V )
11 1 5 6 7 dvmptneg ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ - 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ - 𝐷 ) )
12 1 2 3 4 8 10 11 dvmptadd ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + - 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 + - 𝐷 ) ) )
13 2 5 negsubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 + - 𝐶 ) = ( 𝐴 − 𝐶 ) )
14 13 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + - 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 − 𝐶 ) ) )
15 14 oveq2d ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + - 𝐶 ) ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 − 𝐶 ) ) ) )
16 1 2 3 4 dvmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
17 1 5 6 7 dvmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ ℂ )
18 16 17 negsubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐵 + - 𝐷 ) = ( 𝐵 − 𝐷 ) )
19 18 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 + - 𝐷 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 − 𝐷 ) ) )
20 12 15 19 3eqtr3d ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 − 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 − 𝐷 ) ) )