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=AballabsR
dv11cn.a φA
dv11cn.r φR*
dv11cn.f φF:X
dv11cn.g φG:X
dv11cn.d φdomF=X
dv11cn.e φDF=DG
dv11cn.c φCX
dv11cn.p φFC=GC
Assertion dv11cn φF=G

Proof

Step Hyp Ref Expression
1 dv11cn.x X=AballabsR
2 dv11cn.a φA
3 dv11cn.r φR*
4 dv11cn.f φF:X
5 dv11cn.g φG:X
6 dv11cn.d φdomF=X
7 dv11cn.e φDF=DG
8 dv11cn.c φCX
9 dv11cn.p φFC=GC
10 4 ffnd φFFnX
11 5 ffnd φGFnX
12 1 ovexi XV
13 12 a1i φXV
14 inidm XX=X
15 10 11 13 13 14 offn φFfGFnX
16 0cn 0
17 fnconstg 0X×0FnX
18 16 17 mp1i φX×0FnX
19 subcl xyxy
20 19 adantl φxyxy
21 20 4 5 13 13 14 off φFfG:X
22 21 ffvelrnda φxXFfGx
23 8 anim1ci φxXxXCX
24 cnxmet abs∞Met
25 blssm abs∞MetAR*AballabsR
26 24 2 3 25 mp3an2i φAballabsR
27 1 26 eqsstrid φX
28 4 ffvelrnda φxXFx
29 5 ffvelrnda φxXGx
30 4 feqmptd φF=xXFx
31 5 feqmptd φG=xXGx
32 13 28 29 30 31 offval2 φFfG=xXFxGx
33 32 oveq2d φDFfG=dxXFxGxdx
34 cnelprrecn
35 34 a1i φ
36 fvexd φxXFxV
37 30 oveq2d φDF=dxXFxdx
38 dvfcn F:domF
39 6 feq2d φF:domFF:X
40 38 39 mpbii φF:X
41 40 feqmptd φDF=xXFx
42 37 41 eqtr3d φdxXFxdx=xXFx
43 31 oveq2d φDG=dxXGxdx
44 7 41 43 3eqtr3rd φdxXGxdx=xXFx
45 35 28 36 42 29 36 44 dvmptsub φdxXFxGxdx=xXFxFx
46 40 ffvelrnda φxXFx
47 46 subidd φxXFxFx=0
48 47 mpteq2dva φxXFxFx=xX0
49 fconstmpt X×0=xX0
50 48 49 eqtr4di φxXFxFx=X×0
51 33 45 50 3eqtrd φDFfG=X×0
52 51 dmeqd φdomFfG=domX×0
53 snnzg 00
54 dmxp 0domX×0=X
55 16 53 54 mp2b domX×0=X
56 52 55 eqtrdi φdomFfG=X
57 eqimss2 domFfG=XXdomFfG
58 56 57 syl φXdomFfG
59 0red φ0
60 51 fveq1d φFfGx=X×0x
61 c0ex 0V
62 61 fvconst2 xXX×0x=0
63 60 62 sylan9eq φxXFfGx=0
64 63 abs00bd φxXFfGx=0
65 0le0 00
66 64 65 eqbrtrdi φxXFfGx0
67 27 21 2 3 1 58 59 66 dvlipcn φxXCXFfGxFfGC0xC
68 23 67 syldan φxXFfGxFfGC0xC
69 32 fveq1d φFfGC=xXFxGxC
70 fveq2 x=CFx=FC
71 fveq2 x=CGx=GC
72 70 71 oveq12d x=CFxGx=FCGC
73 eqid xXFxGx=xXFxGx
74 ovex FCGCV
75 72 73 74 fvmpt CXxXFxGxC=FCGC
76 8 75 syl φxXFxGxC=FCGC
77 4 8 ffvelrnd φFC
78 77 9 subeq0bd φFCGC=0
79 69 76 78 3eqtrd φFfGC=0
80 79 adantr φxXFfGC=0
81 80 oveq2d φxXFfGxFfGC=FfGx0
82 22 subid1d φxXFfGx0=FfGx
83 81 82 eqtrd φxXFfGxFfGC=FfGx
84 83 fveq2d φxXFfGxFfGC=FfGx
85 27 sselda φxXx
86 27 8 sseldd φC
87 86 adantr φxXC
88 85 87 subcld φxXxC
89 88 abscld φxXxC
90 89 recnd φxXxC
91 90 mul02d φxX0xC=0
92 68 84 91 3brtr3d φxXFfGx0
93 22 absge0d φxX0FfGx
94 22 abscld φxXFfGx
95 0re 0
96 letri3 FfGx0FfGx=0FfGx00FfGx
97 94 95 96 sylancl φxXFfGx=0FfGx00FfGx
98 92 93 97 mpbir2and φxXFfGx=0
99 22 98 abs00d φxXFfGx=0
100 62 adantl φxXX×0x=0
101 99 100 eqtr4d φxXFfGx=X×0x
102 15 18 101 eqfnfvd φFfG=X×0
103 ofsubeq0 XVF:XG:XFfG=X×0F=G
104 12 4 5 103 mp3an2i φFfG=X×0F=G
105 102 104 mpbid φF=G