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 \circ -) R$
	dv11cn.a	$⊢ φ \to A \in ℂ$
	dv11cn.r	$⊢ φ \to R \in ℝ^{*}$
	dv11cn.f	$⊢ φ \to F : X ⟶ ℂ$
	dv11cn.g	$⊢ φ \to G : X ⟶ ℂ$
	dv11cn.d	$⊢ φ \to dom F_{ℂ}^{'} = X$
	dv11cn.e	$⊢ φ \to ℂ D F = ℂ D G$
	dv11cn.c	$⊢ φ \to C \in X$
	dv11cn.p	$⊢ φ \to F (C) = G (C)$
Assertion	dv11cn	$⊢ φ \to F = G$

Proof

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

Metamath Proof Explorer

Theorem dv11cn

Proof