This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 )
dv11cn.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
dv11cn.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
dv11cn.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
dv11cn.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
dv11cn.d ⊢ ( 𝜑 → dom ( ℂ D 𝐹 ) = 𝑋 )
dv11cn.e ⊢ ( 𝜑 → ( ℂ D 𝐹 ) = ( ℂ D 𝐺 ) )
dv11cn.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
dv11cn.p ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) = ( 𝐺 ‘ 𝐶 ) )
Assertion dv11cn ( 𝜑 → 𝐹 = 𝐺 )

Proof

Step Hyp Ref Expression
1 dv11cn.x ⊢ 𝑋 = ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 )
2 dv11cn.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
3 dv11cn.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
4 dv11cn.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
5 dv11cn.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
6 dv11cn.d ⊢ ( 𝜑 → dom ( ℂ D 𝐹 ) = 𝑋 )
7 dv11cn.e ⊢ ( 𝜑 → ( ℂ D 𝐹 ) = ( ℂ D 𝐺 ) )
8 dv11cn.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
9 dv11cn.p ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) = ( 𝐺 ‘ 𝐶 ) )
10 4 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
11 5 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝑋 )
12 1 ovexi ⊢ 𝑋 ∈ V
13 12 a1i ⊢ ( 𝜑 → 𝑋 ∈ V )
14 inidm ⊢ ( 𝑋 ∩ 𝑋 ) = 𝑋
15 10 11 13 13 14 offn ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐺 ) Fn 𝑋 )
16 0cn ⊢ 0 ∈ ℂ
17 fnconstg ⊢ ( 0 ∈ ℂ → ( 𝑋 × { 0 } ) Fn 𝑋 )
18 16 17 mp1i ⊢ ( 𝜑 → ( 𝑋 × { 0 } ) Fn 𝑋 )
19 subcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 − 𝑦 ) ∈ ℂ )
20 19 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 − 𝑦 ) ∈ ℂ )
21 20 4 5 13 13 14 off ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐺 ) : 𝑋 ⟶ ℂ )
22 21 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ∈ ℂ )
23 8 anim1ci ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) )
24 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
25 blssm ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℝ* ) → ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ⊆ ℂ )
26 24 2 3 25 mp3an2i ⊢ ( 𝜑 → ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ⊆ ℂ )
27 1 26 eqsstrid ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
28 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
29 5 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
30 4 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) )
31 5 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) )
32 13 28 29 30 31 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) )
33 32 oveq2d ⊢ ( 𝜑 → ( ℂ D ( 𝐹 ∘f − 𝐺 ) ) = ( ℂ D ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ) )
34 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
35 34 a1i ⊢ ( 𝜑 → ℂ ∈ { ℝ , ℂ } )
36 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ℂ D 𝐹 ) ‘ 𝑥 ) ∈ V )
37 30 oveq2d ⊢ ( 𝜑 → ( ℂ D 𝐹 ) = ( ℂ D ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
38 dvfcn ⊢ ( ℂ D 𝐹 ) : dom ( ℂ D 𝐹 ) ⟶ ℂ
39 6 feq2d ⊢ ( 𝜑 → ( ( ℂ D 𝐹 ) : dom ( ℂ D 𝐹 ) ⟶ ℂ ↔ ( ℂ D 𝐹 ) : 𝑋 ⟶ ℂ ) )
40 38 39 mpbii ⊢ ( 𝜑 → ( ℂ D 𝐹 ) : 𝑋 ⟶ ℂ )
41 40 feqmptd ⊢ ( 𝜑 → ( ℂ D 𝐹 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ℂ D 𝐹 ) ‘ 𝑥 ) ) )
42 37 41 eqtr3d ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ℂ D 𝐹 ) ‘ 𝑥 ) ) )
43 31 oveq2d ⊢ ( 𝜑 → ( ℂ D 𝐺 ) = ( ℂ D ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) ) )
44 7 41 43 3eqtr3rd ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ℂ D 𝐹 ) ‘ 𝑥 ) ) )
45 35 28 36 42 29 36 44 dvmptsub ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( ℂ D 𝐹 ) ‘ 𝑥 ) − ( ( ℂ D 𝐹 ) ‘ 𝑥 ) ) ) )
46 40 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ℂ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
47 46 subidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( ℂ D 𝐹 ) ‘ 𝑥 ) − ( ( ℂ D 𝐹 ) ‘ 𝑥 ) ) = 0 )
48 47 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( ( ℂ D 𝐹 ) ‘ 𝑥 ) − ( ( ℂ D 𝐹 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
49 fconstmpt ⊢ ( 𝑋 × { 0 } ) = ( 𝑥 ∈ 𝑋 ↦ 0 )
50 48 49 eqtr4di ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( ( ℂ D 𝐹 ) ‘ 𝑥 ) − ( ( ℂ D 𝐹 ) ‘ 𝑥 ) ) ) = ( 𝑋 × { 0 } ) )
51 33 45 50 3eqtrd ⊢ ( 𝜑 → ( ℂ D ( 𝐹 ∘f − 𝐺 ) ) = ( 𝑋 × { 0 } ) )
52 51 dmeqd ⊢ ( 𝜑 → dom ( ℂ D ( 𝐹 ∘f − 𝐺 ) ) = dom ( 𝑋 × { 0 } ) )
53 snnzg ⊢ ( 0 ∈ ℂ → { 0 } ≠ ∅ )
54 dmxp ⊢ ( { 0 } ≠ ∅ → dom ( 𝑋 × { 0 } ) = 𝑋 )
55 16 53 54 mp2b ⊢ dom ( 𝑋 × { 0 } ) = 𝑋
56 52 55 eqtrdi ⊢ ( 𝜑 → dom ( ℂ D ( 𝐹 ∘f − 𝐺 ) ) = 𝑋 )
57 eqimss2 ⊢ ( dom ( ℂ D ( 𝐹 ∘f − 𝐺 ) ) = 𝑋 → 𝑋 ⊆ dom ( ℂ D ( 𝐹 ∘f − 𝐺 ) ) )
58 56 57 syl ⊢ ( 𝜑 → 𝑋 ⊆ dom ( ℂ D ( 𝐹 ∘f − 𝐺 ) ) )
59 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
60 51 fveq1d ⊢ ( 𝜑 → ( ( ℂ D ( 𝐹 ∘f − 𝐺 ) ) ‘ 𝑥 ) = ( ( 𝑋 × { 0 } ) ‘ 𝑥 ) )
61 c0ex ⊢ 0 ∈ V
62 61 fvconst2 ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑋 × { 0 } ) ‘ 𝑥 ) = 0 )
63 60 62 sylan9eq ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ℂ D ( 𝐹 ∘f − 𝐺 ) ) ‘ 𝑥 ) = 0 )
64 63 abs00bd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( ℂ D ( 𝐹 ∘f − 𝐺 ) ) ‘ 𝑥 ) ) = 0 )
65 0le0 ⊢ 0 ≤ 0
66 64 65 eqbrtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( ℂ D ( 𝐹 ∘f − 𝐺 ) ) ‘ 𝑥 ) ) ≤ 0 )
67 27 21 2 3 1 58 59 66 dvlipcn ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( abs ‘ ( ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) − ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝐶 ) ) ) ≤ ( 0 · ( abs ‘ ( 𝑥 − 𝐶 ) ) ) )
68 23 67 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) − ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝐶 ) ) ) ≤ ( 0 · ( abs ‘ ( 𝑥 − 𝐶 ) ) ) )
69 32 fveq1d ⊢ ( 𝜑 → ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝐶 ) = ( ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝐶 ) )
70 fveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐶 ) )
71 fveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝐶 ) )
72 70 71 oveq12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝐶 ) − ( 𝐺 ‘ 𝐶 ) ) )
73 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) )
74 ovex ⊢ ( ( 𝐹 ‘ 𝐶 ) − ( 𝐺 ‘ 𝐶 ) ) ∈ V
75 72 73 74 fvmpt ⊢ ( 𝐶 ∈ 𝑋 → ( ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝐶 ) = ( ( 𝐹 ‘ 𝐶 ) − ( 𝐺 ‘ 𝐶 ) ) )
76 8 75 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝐶 ) = ( ( 𝐹 ‘ 𝐶 ) − ( 𝐺 ‘ 𝐶 ) ) )
77 4 8 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
78 77 9 subeq0bd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) − ( 𝐺 ‘ 𝐶 ) ) = 0 )
79 69 76 78 3eqtrd ⊢ ( 𝜑 → ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝐶 ) = 0 )
80 79 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝐶 ) = 0 )
81 80 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) − ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝐶 ) ) = ( ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) − 0 ) )
82 22 subid1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) − 0 ) = ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) )
83 81 82 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) − ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝐶 ) ) = ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) )
84 83 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) − ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝐶 ) ) ) = ( abs ‘ ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ) )
85 27 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ℂ )
86 27 8 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
87 86 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
88 85 87 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 − 𝐶 ) ∈ ℂ )
89 88 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝑥 − 𝐶 ) ) ∈ ℝ )
90 89 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝑥 − 𝐶 ) ) ∈ ℂ )
91 90 mul02d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 0 · ( abs ‘ ( 𝑥 − 𝐶 ) ) ) = 0 )
92 68 84 91 3brtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ) ≤ 0 )
93 22 absge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( abs ‘ ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ) )
94 22 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ) ∈ ℝ )
95 0re ⊢ 0 ∈ ℝ
96 letri3 ⊢ ( ( ( abs ‘ ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( abs ‘ ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ) = 0 ↔ ( ( abs ‘ ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ) ≤ 0 ∧ 0 ≤ ( abs ‘ ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ) ) ) )
97 94 95 96 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( abs ‘ ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ) = 0 ↔ ( ( abs ‘ ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ) ≤ 0 ∧ 0 ≤ ( abs ‘ ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ) ) ) )
98 92 93 97 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ) = 0 )
99 22 98 abs00d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) = 0 )
100 62 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑋 × { 0 } ) ‘ 𝑥 ) = 0 )
101 99 100 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) = ( ( 𝑋 × { 0 } ) ‘ 𝑥 ) )
102 15 18 101 eqfnfvd ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐺 ) = ( 𝑋 × { 0 } ) )
103 ofsubeq0 ⊢ ( ( 𝑋 ∈ V ∧ 𝐹 : 𝑋 ⟶ ℂ ∧ 𝐺 : 𝑋 ⟶ ℂ ) → ( ( 𝐹 ∘f − 𝐺 ) = ( 𝑋 × { 0 } ) ↔ 𝐹 = 𝐺 ) )
104 12 4 5 103 mp3an2i ⊢ ( 𝜑 → ( ( 𝐹 ∘f − 𝐺 ) = ( 𝑋 × { 0 } ) ↔ 𝐹 = 𝐺 ) )
105 102 104 mpbid ⊢ ( 𝜑 → 𝐹 = 𝐺 )