Metamath Proof Explorer


Theorem dvfval

Description: Value and set bounds on the derivative operator. (Contributed by Mario Carneiro, 7-Aug-2014) (Revised by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses dvval.t T = K 𝑡 S
dvval.k K = TopOpen fld
Assertion dvfval S F : A A S S D F = x int T A x × z A x F z F x z x lim x S D F int T A ×

Proof

Step Hyp Ref Expression
1 dvval.t T = K 𝑡 S
2 dvval.k K = TopOpen fld
3 df-dv D = s 𝒫 , f 𝑝𝑚 s x int TopOpen fld 𝑡 s dom f x × z dom f x f z f x z x lim x
4 3 a1i S F : A A S D = s 𝒫 , f 𝑝𝑚 s x int TopOpen fld 𝑡 s dom f x × z dom f x f z f x z x lim x
5 2 oveq1i K 𝑡 s = TopOpen fld 𝑡 s
6 simprl S F : A A S s = S f = F s = S
7 6 oveq2d S F : A A S s = S f = F K 𝑡 s = K 𝑡 S
8 7 1 eqtr4di S F : A A S s = S f = F K 𝑡 s = T
9 5 8 eqtr3id S F : A A S s = S f = F TopOpen fld 𝑡 s = T
10 9 fveq2d S F : A A S s = S f = F int TopOpen fld 𝑡 s = int T
11 simprr S F : A A S s = S f = F f = F
12 11 dmeqd S F : A A S s = S f = F dom f = dom F
13 simpl2 S F : A A S s = S f = F F : A
14 13 fdmd S F : A A S s = S f = F dom F = A
15 12 14 eqtrd S F : A A S s = S f = F dom f = A
16 10 15 fveq12d S F : A A S s = S f = F int TopOpen fld 𝑡 s dom f = int T A
17 15 difeq1d S F : A A S s = S f = F dom f x = A x
18 11 fveq1d S F : A A S s = S f = F f z = F z
19 11 fveq1d S F : A A S s = S f = F f x = F x
20 18 19 oveq12d S F : A A S s = S f = F f z f x = F z F x
21 20 oveq1d S F : A A S s = S f = F f z f x z x = F z F x z x
22 17 21 mpteq12dv S F : A A S s = S f = F z dom f x f z f x z x = z A x F z F x z x
23 22 oveq1d S F : A A S s = S f = F z dom f x f z f x z x lim x = z A x F z F x z x lim x
24 23 xpeq2d S F : A A S s = S f = F x × z dom f x f z f x z x lim x = x × z A x F z F x z x lim x
25 16 24 iuneq12d S F : A A S s = S f = F x int TopOpen fld 𝑡 s dom f x × z dom f x f z f x z x lim x = x int T A x × z A x F z F x z x lim x
26 simpr S F : A A S s = S s = S
27 26 oveq2d S F : A A S s = S 𝑝𝑚 s = 𝑝𝑚 S
28 simp1 S F : A A S S
29 cnex V
30 29 elpw2 S 𝒫 S
31 28 30 sylibr S F : A A S S 𝒫
32 29 a1i S F : A A S V
33 simp2 S F : A A S F : A
34 simp3 S F : A A S A S
35 elpm2r V S 𝒫 F : A A S F 𝑝𝑚 S
36 32 31 33 34 35 syl22anc S F : A A S F 𝑝𝑚 S
37 limccl z A x F z F x z x lim x
38 xpss2 z A x F z F x z x lim x x × z A x F z F x z x lim x x ×
39 37 38 ax-mp x × z A x F z F x z x lim x x ×
40 39 rgenw x int T A x × z A x F z F x z x lim x x ×
41 ss2iun x int T A x × z A x F z F x z x lim x x × x int T A x × z A x F z F x z x lim x x int T A x ×
42 40 41 ax-mp x int T A x × z A x F z F x z x lim x x int T A x ×
43 iunxpconst x int T A x × = int T A ×
44 42 43 sseqtri x int T A x × z A x F z F x z x lim x int T A ×
45 44 a1i S F : A A S x int T A x × z A x F z F x z x lim x int T A ×
46 fvex int T A V
47 46 29 xpex int T A × V
48 47 ssex x int T A x × z A x F z F x z x lim x int T A × x int T A x × z A x F z F x z x lim x V
49 45 48 syl S F : A A S x int T A x × z A x F z F x z x lim x V
50 4 25 27 31 36 49 ovmpodx S F : A A S S D F = x int T A x × z A x F z F x z x lim x
51 50 45 eqsstrd S F : A A S S D F int T A ×
52 50 51 jca S F : A A S S D F = x int T A x × z A x F z F x z x lim x S D F int T A ×