Metamath Proof Explorer


Theorem dvmptconst

Description: Function-builder for derivative: derivative of a constant. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvmptconst.s φ S
dvmptconst.a φ A TopOpen fld 𝑡 S
dvmptconst.b φ B
Assertion dvmptconst φ dx A B dS x = x A 0

Proof

Step Hyp Ref Expression
1 dvmptconst.s φ S
2 dvmptconst.a φ A TopOpen fld 𝑡 S
3 dvmptconst.b φ B
4 3 adantr φ x S B
5 0red φ x S 0
6 1 3 dvmptc φ dx S B dS x = x S 0
7 eqid TopOpen fld = TopOpen fld
8 7 cnfldtopon TopOpen fld TopOn
9 8 a1i φ TopOpen fld TopOn
10 ax-resscn
11 sseq1 S = S
12 10 11 mpbiri S = S
13 eqimss S = S
14 12 13 pm3.2i S = S S = S
15 elpri S S = S =
16 1 15 syl φ S = S =
17 pm3.44 S = S S = S S = S = S
18 14 16 17 mpsyl φ S
19 resttopon TopOpen fld TopOn S TopOpen fld 𝑡 S TopOn S
20 9 18 19 syl2anc φ TopOpen fld 𝑡 S TopOn S
21 toponss TopOpen fld 𝑡 S TopOn S A TopOpen fld 𝑡 S A S
22 20 2 21 syl2anc φ A S
23 eqid TopOpen fld 𝑡 S = TopOpen fld 𝑡 S
24 1 4 5 6 22 23 7 2 dvmptres φ dx A B dS x = x A 0