Metamath Proof Explorer

Theorem dvmptadd

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

Ref Expression
Hypotheses dvmptadd.s ⊢φ→S∈ℝℂ
dvmptadd.a ⊢φ∧x∈X→A∈ℂ
dvmptadd.b ⊢φ∧x∈X→B∈V
dvmptadd.da ⊢φ→dx∈XAdSx=x∈X⟼B
dvmptadd.c ⊢φ∧x∈X→C∈ℂ
dvmptadd.d ⊢φ∧x∈X→D∈W
dvmptadd.dc ⊢φ→dx∈XCdSx=x∈X⟼D
Assertion dvmptadd ⊢φ→dx∈XA+CdSx=x∈X⟼B+D

Proof

Step Hyp Ref Expression
1 dvmptadd.s ⊢φ→S∈ℝℂ
2 dvmptadd.a ⊢φ∧x∈X→A∈ℂ
3 dvmptadd.b ⊢φ∧x∈X→B∈V
4 dvmptadd.da ⊢φ→dx∈XAdSx=x∈X⟼B
5 dvmptadd.c ⊢φ∧x∈X→C∈ℂ
6 dvmptadd.d ⊢φ∧x∈X→D∈W
7 dvmptadd.dc ⊢φ→dx∈XCdSx=x∈X⟼D
8 2 fmpttd ⊢φ→x∈X⟼A:X⟶ℂ
9 5 fmpttd ⊢φ→x∈X⟼C:X⟶ℂ
10 4 dmeqd ⊢φ→dom⁡dx∈XAdSx=dom⁡x∈X⟼B
11 3 ralrimiva ⊢φ→∀x∈XB∈V
12 dmmptg ⊢∀x∈XB∈V→dom⁡x∈X⟼B=X
13 11 12 syl ⊢φ→dom⁡x∈X⟼B=X
14 10 13 eqtrd ⊢φ→dom⁡dx∈XAdSx=X
15 7 dmeqd ⊢φ→dom⁡dx∈XCdSx=dom⁡x∈X⟼D
16 6 ralrimiva ⊢φ→∀x∈XD∈W
17 dmmptg ⊢∀x∈XD∈W→dom⁡x∈X⟼D=X
18 16 17 syl ⊢φ→dom⁡x∈X⟼D=X
19 15 18 eqtrd ⊢φ→dom⁡dx∈XCdSx=X
20 1 8 9 14 19 dvaddf ⊢φ→SDx∈X⟼A+fx∈X⟼C=dx∈XAdSx+fdx∈XCdSx
21 ovex ⊢dx∈XCdSx∈V
22 21 dmex ⊢dom⁡dx∈XCdSx∈V
23 19 22 eqeltrrdi ⊢φ→X∈V
24 eqidd ⊢φ→x∈X⟼A=x∈X⟼A
25 eqidd ⊢φ→x∈X⟼C=x∈X⟼C
26 23 2 5 24 25 offval2 ⊢φ→x∈X⟼A+fx∈X⟼C=x∈X⟼A+C
27 26 oveq2d ⊢φ→SDx∈X⟼A+fx∈X⟼C=dx∈XA+CdSx
28 23 3 6 4 7 offval2 ⊢φ→dx∈XAdSx+fdx∈XCdSx=x∈X⟼B+D
29 20 27 28 3eqtr3d ⊢φ→dx∈XA+CdSx=x∈X⟼B+D