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 )