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	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ∘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	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
29	5	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
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	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ℂ 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	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
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	⊢ ( 𝜑 → 𝐹 = 𝐺 )