Metamath Proof Explorer


Theorem dv11cn

Description: Two functions defined on a ball whose derivatives are the same and which are equal at any given point C in the ball must be equal everywhere. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Hypotheses dv11cn.x
|- X = ( A ( ball ` ( abs o. - ) ) R )
dv11cn.a
|- ( ph -> A e. CC )
dv11cn.r
|- ( ph -> R e. RR* )
dv11cn.f
|- ( ph -> F : X --> CC )
dv11cn.g
|- ( ph -> G : X --> CC )
dv11cn.d
|- ( ph -> dom ( CC _D F ) = X )
dv11cn.e
|- ( ph -> ( CC _D F ) = ( CC _D G ) )
dv11cn.c
|- ( ph -> C e. X )
dv11cn.p
|- ( ph -> ( F ` C ) = ( G ` C ) )
Assertion dv11cn
|- ( ph -> F = G )

Proof

Step Hyp Ref Expression
1 dv11cn.x
 |-  X = ( A ( ball ` ( abs o. - ) ) R )
2 dv11cn.a
 |-  ( ph -> A e. CC )
3 dv11cn.r
 |-  ( ph -> R e. RR* )
4 dv11cn.f
 |-  ( ph -> F : X --> CC )
5 dv11cn.g
 |-  ( ph -> G : X --> CC )
6 dv11cn.d
 |-  ( ph -> dom ( CC _D F ) = X )
7 dv11cn.e
 |-  ( ph -> ( CC _D F ) = ( CC _D G ) )
8 dv11cn.c
 |-  ( ph -> C e. X )
9 dv11cn.p
 |-  ( ph -> ( F ` C ) = ( G ` C ) )
10 4 ffnd
 |-  ( ph -> F Fn X )
11 5 ffnd
 |-  ( ph -> G Fn X )
12 1 ovexi
 |-  X e. _V
13 12 a1i
 |-  ( ph -> X e. _V )
14 inidm
 |-  ( X i^i X ) = X
15 10 11 13 13 14 offn
 |-  ( ph -> ( F oF - G ) Fn X )
16 0cn
 |-  0 e. CC
17 fnconstg
 |-  ( 0 e. CC -> ( X X. { 0 } ) Fn X )
18 16 17 mp1i
 |-  ( ph -> ( X X. { 0 } ) Fn X )
19 subcl
 |-  ( ( x e. CC /\ y e. CC ) -> ( x - y ) e. CC )
20 19 adantl
 |-  ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x - y ) e. CC )
21 20 4 5 13 13 14 off
 |-  ( ph -> ( F oF - G ) : X --> CC )
22 21 ffvelrnda
 |-  ( ( ph /\ x e. X ) -> ( ( F oF - G ) ` x ) e. CC )
23 8 anim1ci
 |-  ( ( ph /\ x e. X ) -> ( x e. X /\ C e. X ) )
24 cnxmet
 |-  ( abs o. - ) e. ( *Met ` CC )
25 blssm
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ A e. CC /\ R e. RR* ) -> ( A ( ball ` ( abs o. - ) ) R ) C_ CC )
26 24 2 3 25 mp3an2i
 |-  ( ph -> ( A ( ball ` ( abs o. - ) ) R ) C_ CC )
27 1 26 eqsstrid
 |-  ( ph -> X C_ CC )
28 4 ffvelrnda
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. CC )
29 5 ffvelrnda
 |-  ( ( ph /\ x e. X ) -> ( G ` x ) e. CC )
30 4 feqmptd
 |-  ( ph -> F = ( x e. X |-> ( F ` x ) ) )
31 5 feqmptd
 |-  ( ph -> G = ( x e. X |-> ( G ` x ) ) )
32 13 28 29 30 31 offval2
 |-  ( ph -> ( F oF - G ) = ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) )
33 32 oveq2d
 |-  ( ph -> ( CC _D ( F oF - G ) ) = ( CC _D ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) ) )
34 cnelprrecn
 |-  CC e. { RR , CC }
35 34 a1i
 |-  ( ph -> CC e. { RR , CC } )
36 fvexd
 |-  ( ( ph /\ x e. X ) -> ( ( CC _D F ) ` x ) e. _V )
37 30 oveq2d
 |-  ( ph -> ( CC _D F ) = ( CC _D ( x e. X |-> ( F ` x ) ) ) )
38 dvfcn
 |-  ( CC _D F ) : dom ( CC _D F ) --> CC
39 6 feq2d
 |-  ( ph -> ( ( CC _D F ) : dom ( CC _D F ) --> CC <-> ( CC _D F ) : X --> CC ) )
40 38 39 mpbii
 |-  ( ph -> ( CC _D F ) : X --> CC )
41 40 feqmptd
 |-  ( ph -> ( CC _D F ) = ( x e. X |-> ( ( CC _D F ) ` x ) ) )
42 37 41 eqtr3d
 |-  ( ph -> ( CC _D ( x e. X |-> ( F ` x ) ) ) = ( x e. X |-> ( ( CC _D F ) ` x ) ) )
43 31 oveq2d
 |-  ( ph -> ( CC _D G ) = ( CC _D ( x e. X |-> ( G ` x ) ) ) )
44 7 41 43 3eqtr3rd
 |-  ( ph -> ( CC _D ( x e. X |-> ( G ` x ) ) ) = ( x e. X |-> ( ( CC _D F ) ` x ) ) )
45 35 28 36 42 29 36 44 dvmptsub
 |-  ( ph -> ( CC _D ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) ) = ( x e. X |-> ( ( ( CC _D F ) ` x ) - ( ( CC _D F ) ` x ) ) ) )
46 40 ffvelrnda
 |-  ( ( ph /\ x e. X ) -> ( ( CC _D F ) ` x ) e. CC )
47 46 subidd
 |-  ( ( ph /\ x e. X ) -> ( ( ( CC _D F ) ` x ) - ( ( CC _D F ) ` x ) ) = 0 )
48 47 mpteq2dva
 |-  ( ph -> ( x e. X |-> ( ( ( CC _D F ) ` x ) - ( ( CC _D F ) ` x ) ) ) = ( x e. X |-> 0 ) )
49 fconstmpt
 |-  ( X X. { 0 } ) = ( x e. X |-> 0 )
50 48 49 eqtr4di
 |-  ( ph -> ( x e. X |-> ( ( ( CC _D F ) ` x ) - ( ( CC _D F ) ` x ) ) ) = ( X X. { 0 } ) )
51 33 45 50 3eqtrd
 |-  ( ph -> ( CC _D ( F oF - G ) ) = ( X X. { 0 } ) )
52 51 dmeqd
 |-  ( ph -> dom ( CC _D ( F oF - G ) ) = dom ( X X. { 0 } ) )
53 snnzg
 |-  ( 0 e. CC -> { 0 } =/= (/) )
54 dmxp
 |-  ( { 0 } =/= (/) -> dom ( X X. { 0 } ) = X )
55 16 53 54 mp2b
 |-  dom ( X X. { 0 } ) = X
56 52 55 eqtrdi
 |-  ( ph -> dom ( CC _D ( F oF - G ) ) = X )
57 eqimss2
 |-  ( dom ( CC _D ( F oF - G ) ) = X -> X C_ dom ( CC _D ( F oF - G ) ) )
58 56 57 syl
 |-  ( ph -> X C_ dom ( CC _D ( F oF - G ) ) )
59 0red
 |-  ( ph -> 0 e. RR )
60 51 fveq1d
 |-  ( ph -> ( ( CC _D ( F oF - G ) ) ` x ) = ( ( X X. { 0 } ) ` x ) )
61 c0ex
 |-  0 e. _V
62 61 fvconst2
 |-  ( x e. X -> ( ( X X. { 0 } ) ` x ) = 0 )
63 60 62 sylan9eq
 |-  ( ( ph /\ x e. X ) -> ( ( CC _D ( F oF - G ) ) ` x ) = 0 )
64 63 abs00bd
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( ( CC _D ( F oF - G ) ) ` x ) ) = 0 )
65 0le0
 |-  0 <_ 0
66 64 65 eqbrtrdi
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( ( CC _D ( F oF - G ) ) ` x ) ) <_ 0 )
67 27 21 2 3 1 58 59 66 dvlipcn
 |-  ( ( ph /\ ( x e. X /\ C e. X ) ) -> ( abs ` ( ( ( F oF - G ) ` x ) - ( ( F oF - G ) ` C ) ) ) <_ ( 0 x. ( abs ` ( x - C ) ) ) )
68 23 67 syldan
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( ( ( F oF - G ) ` x ) - ( ( F oF - G ) ` C ) ) ) <_ ( 0 x. ( abs ` ( x - C ) ) ) )
69 32 fveq1d
 |-  ( ph -> ( ( F oF - G ) ` C ) = ( ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) ` C ) )
70 fveq2
 |-  ( x = C -> ( F ` x ) = ( F ` C ) )
71 fveq2
 |-  ( x = C -> ( G ` x ) = ( G ` C ) )
72 70 71 oveq12d
 |-  ( x = C -> ( ( F ` x ) - ( G ` x ) ) = ( ( F ` C ) - ( G ` C ) ) )
73 eqid
 |-  ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) = ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) )
74 ovex
 |-  ( ( F ` C ) - ( G ` C ) ) e. _V
75 72 73 74 fvmpt
 |-  ( C e. X -> ( ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) ` C ) = ( ( F ` C ) - ( G ` C ) ) )
76 8 75 syl
 |-  ( ph -> ( ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) ` C ) = ( ( F ` C ) - ( G ` C ) ) )
77 4 8 ffvelrnd
 |-  ( ph -> ( F ` C ) e. CC )
78 77 9 subeq0bd
 |-  ( ph -> ( ( F ` C ) - ( G ` C ) ) = 0 )
79 69 76 78 3eqtrd
 |-  ( ph -> ( ( F oF - G ) ` C ) = 0 )
80 79 adantr
 |-  ( ( ph /\ x e. X ) -> ( ( F oF - G ) ` C ) = 0 )
81 80 oveq2d
 |-  ( ( ph /\ x e. X ) -> ( ( ( F oF - G ) ` x ) - ( ( F oF - G ) ` C ) ) = ( ( ( F oF - G ) ` x ) - 0 ) )
82 22 subid1d
 |-  ( ( ph /\ x e. X ) -> ( ( ( F oF - G ) ` x ) - 0 ) = ( ( F oF - G ) ` x ) )
83 81 82 eqtrd
 |-  ( ( ph /\ x e. X ) -> ( ( ( F oF - G ) ` x ) - ( ( F oF - G ) ` C ) ) = ( ( F oF - G ) ` x ) )
84 83 fveq2d
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( ( ( F oF - G ) ` x ) - ( ( F oF - G ) ` C ) ) ) = ( abs ` ( ( F oF - G ) ` x ) ) )
85 27 sselda
 |-  ( ( ph /\ x e. X ) -> x e. CC )
86 27 8 sseldd
 |-  ( ph -> C e. CC )
87 86 adantr
 |-  ( ( ph /\ x e. X ) -> C e. CC )
88 85 87 subcld
 |-  ( ( ph /\ x e. X ) -> ( x - C ) e. CC )
89 88 abscld
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( x - C ) ) e. RR )
90 89 recnd
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( x - C ) ) e. CC )
91 90 mul02d
 |-  ( ( ph /\ x e. X ) -> ( 0 x. ( abs ` ( x - C ) ) ) = 0 )
92 68 84 91 3brtr3d
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( ( F oF - G ) ` x ) ) <_ 0 )
93 22 absge0d
 |-  ( ( ph /\ x e. X ) -> 0 <_ ( abs ` ( ( F oF - G ) ` x ) ) )
94 22 abscld
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( ( F oF - G ) ` x ) ) e. RR )
95 0re
 |-  0 e. RR
96 letri3
 |-  ( ( ( abs ` ( ( F oF - G ) ` x ) ) e. RR /\ 0 e. RR ) -> ( ( abs ` ( ( F oF - G ) ` x ) ) = 0 <-> ( ( abs ` ( ( F oF - G ) ` x ) ) <_ 0 /\ 0 <_ ( abs ` ( ( F oF - G ) ` x ) ) ) ) )
97 94 95 96 sylancl
 |-  ( ( ph /\ x e. X ) -> ( ( abs ` ( ( F oF - G ) ` x ) ) = 0 <-> ( ( abs ` ( ( F oF - G ) ` x ) ) <_ 0 /\ 0 <_ ( abs ` ( ( F oF - G ) ` x ) ) ) ) )
98 92 93 97 mpbir2and
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( ( F oF - G ) ` x ) ) = 0 )
99 22 98 abs00d
 |-  ( ( ph /\ x e. X ) -> ( ( F oF - G ) ` x ) = 0 )
100 62 adantl
 |-  ( ( ph /\ x e. X ) -> ( ( X X. { 0 } ) ` x ) = 0 )
101 99 100 eqtr4d
 |-  ( ( ph /\ x e. X ) -> ( ( F oF - G ) ` x ) = ( ( X X. { 0 } ) ` x ) )
102 15 18 101 eqfnfvd
 |-  ( ph -> ( F oF - G ) = ( X X. { 0 } ) )
103 ofsubeq0
 |-  ( ( X e. _V /\ F : X --> CC /\ G : X --> CC ) -> ( ( F oF - G ) = ( X X. { 0 } ) <-> F = G ) )
104 12 4 5 103 mp3an2i
 |-  ( ph -> ( ( F oF - G ) = ( X X. { 0 } ) <-> F = G ) )
105 102 104 mpbid
 |-  ( ph -> F = G )