dvconstbi

Description: The derivative of a function on S is zero iff it is a constant function. Roughly a biconditional S analogue of dvconst and dveq0 . Corresponds to integration formula " S. 0 _d x = C " in section 4.1 of LarsonHostetlerEdwards p. 278. (Contributed by Steve Rodriguez, 11-Nov-2015)

	Ref	Expression
Hypotheses	dvconstbi.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvconstbi.y	$⊢ φ \to Y : S ⟶ ℂ$
	dvconstbi.dy	$⊢ φ \to dom Y_{S}^{'} = S$
Assertion	dvconstbi	$⊢ φ \to (S D Y = S \times \{0\} \leftrightarrow \exists c \in ℂ Y = S \times \{c\})$

Proof

Step	Hyp	Ref	Expression
1		dvconstbi.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvconstbi.y	$⊢ φ \to Y : S ⟶ ℂ$
3		dvconstbi.dy	$⊢ φ \to dom Y_{S}^{'} = S$
4		elpri	$⊢ S \in \{ℝ, ℂ\} \to (S = ℝ \lor S = ℂ)$
5	1 4	syl	$⊢ φ \to (S = ℝ \lor S = ℂ)$
6		0re	$⊢ 0 \in ℝ$
7		eleq2	$⊢ S = ℝ \to (0 \in S \leftrightarrow 0 \in ℝ)$
8	6 7	mpbiri	$⊢ S = ℝ \to 0 \in S$
9		0cn	$⊢ 0 \in ℂ$
10		eleq2	$⊢ S = ℂ \to (0 \in S \leftrightarrow 0 \in ℂ)$
11	9 10	mpbiri	$⊢ S = ℂ \to 0 \in S$
12	8 11	jaoi	$⊢ (S = ℝ \lor S = ℂ) \to 0 \in S$
13	5 12	syl	$⊢ φ \to 0 \in S$
14		ffvelcdm	$⊢ (Y : S ⟶ ℂ \land 0 \in S) \to Y (0) \in ℂ$
15	2 13 14	syl2anc	$⊢ φ \to Y (0) \in ℂ$
16	15	adantr	$⊢ (φ \land S D Y = S \times \{0\}) \to Y (0) \in ℂ$
17	2	ffnd	$⊢ φ \to Y Fn S$
18	17	adantr	$⊢ (φ \land S D Y = S \times \{0\}) \to Y Fn S$
19		fvex	$⊢ Y (0) \in V$
20		fnconstg	$⊢ Y (0) \in V \to (S \times \{Y (0)\}) Fn S$
21	19 20	mp1i	$⊢ (φ \land S D Y = S \times \{0\}) \to (S \times \{Y (0)\}) Fn S$
22	19	fvconst2	$⊢ y \in S \to (S \times \{Y (0)\}) (y) = Y (0)$
23	22	adantl	$⊢ ((φ \land S D Y = S \times \{0\}) \land y \in S) \to (S \times \{Y (0)\}) (y) = Y (0)$
24		eqid	$⊢ {(abs \circ -) ↾}_{(S \times S)} = {(abs \circ -) ↾}_{(S \times S)}$
25	1 24	sblpnf	$⊢ (φ \land 0 \in S) \to 0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞ = S$
26	13 25	mpdan	$⊢ φ \to 0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞ = S$
27	26	eleq2d	$⊢ φ \to (y \in (0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞) \leftrightarrow y \in S)$
28	27	biimpar	$⊢ (φ \land y \in S) \to y \in (0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞)$
29	13 26	eleqtrrd	$⊢ φ \to 0 \in (0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞)$
30	1	adantr	$⊢ (φ \land S D Y = S \times \{0\}) \to S \in \{ℝ, ℂ\}$
31		ssidd	$⊢ (φ \land S D Y = S \times \{0\}) \to S \subseteq S$
32	2	adantr	$⊢ (φ \land S D Y = S \times \{0\}) \to Y : S ⟶ ℂ$
33	13	adantr	$⊢ (φ \land S D Y = S \times \{0\}) \to 0 \in S$
34		pnfxr	$⊢ +∞ \in ℝ^{*}$
35	34	a1i	$⊢ (φ \land S D Y = S \times \{0\}) \to +∞ \in ℝ^{*}$
36		eqid	$⊢ 0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞ = 0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞$
37	26	adantr	$⊢ (φ \land S D Y = S \times \{0\}) \to 0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞ = S$
38	3	adantr	$⊢ (φ \land S D Y = S \times \{0\}) \to dom Y_{S}^{'} = S$
39	37 38	eqtr4d	$⊢ (φ \land S D Y = S \times \{0\}) \to 0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞ = dom Y_{S}^{'}$
40		eqimss	$⊢ 0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞ = dom Y_{S}^{'} \to 0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞ \subseteq dom Y_{S}^{'}$
41	39 40	syl	$⊢ (φ \land S D Y = S \times \{0\}) \to 0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞ \subseteq dom Y_{S}^{'}$
42	6	a1i	$⊢ (φ \land S D Y = S \times \{0\}) \to 0 \in ℝ$
43	26	eleq2d	$⊢ φ \to (x \in (0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞) \leftrightarrow x \in S)$
44	43	biimpa	$⊢ (φ \land x \in (0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞)) \to x \in S$
45	44	3adant2	$⊢ (φ \land S D Y = S \times \{0\} \land x \in (0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞)) \to x \in S$
46		fveq1	$⊢ S D Y = S \times \{0\} \to Y_{S}^{'} (x) = (S \times \{0\}) (x)$
47		c0ex	$⊢ 0 \in V$
48	47	fvconst2	$⊢ x \in S \to (S \times \{0\}) (x) = 0$
49	46 48	sylan9eq	$⊢ (S D Y = S \times \{0\} \land x \in S) \to Y_{S}^{'} (x) = 0$
50	49 9	eqeltrdi	$⊢ (S D Y = S \times \{0\} \land x \in S) \to Y_{S}^{'} (x) \in ℂ$
51	50	abscld	$⊢ (S D Y = S \times \{0\} \land x \in S) \to \|Y_{S}^{'} (x)\| \in ℝ$
52	49	abs00bd	$⊢ (S D Y = S \times \{0\} \land x \in S) \to \|Y_{S}^{'} (x)\| = 0$
53		eqle	$⊢ (\|Y_{S}^{'} (x)\| \in ℝ \land \|Y_{S}^{'} (x)\| = 0) \to \|Y_{S}^{'} (x)\| \leq 0$
54	51 52 53	syl2anc	$⊢ (S D Y = S \times \{0\} \land x \in S) \to \|Y_{S}^{'} (x)\| \leq 0$
55	54	3adant1	$⊢ (φ \land S D Y = S \times \{0\} \land x \in S) \to \|Y_{S}^{'} (x)\| \leq 0$
56	45 55	syld3an3	$⊢ (φ \land S D Y = S \times \{0\} \land x \in (0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞)) \to \|Y_{S}^{'} (x)\| \leq 0$
57	56	3expa	$⊢ ((φ \land S D Y = S \times \{0\}) \land x \in (0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞)) \to \|Y_{S}^{'} (x)\| \leq 0$
58	30 24 31 32 33 35 36 41 42 57	dvlip2	$⊢ ((φ \land S D Y = S \times \{0\}) \land (0 \in (0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞) \land y \in (0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞))) \to \|Y (0) - Y (y)\| \leq 0 \cdot \|0 - y\|$
59	29 58	sylanr1	$⊢ ((φ \land S D Y = S \times \{0\}) \land (φ \land y \in (0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞))) \to \|Y (0) - Y (y)\| \leq 0 \cdot \|0 - y\|$
60	59	3impdi	$⊢ (φ \land S D Y = S \times \{0\} \land y \in (0 ball ({(abs \circ -) ↾}_{(S \times S)}) +∞)) \to \|Y (0) - Y (y)\| \leq 0 \cdot \|0 - y\|$
61	28 60	syl3an3	$⊢ (φ \land S D Y = S \times \{0\} \land (φ \land y \in S)) \to \|Y (0) - Y (y)\| \leq 0 \cdot \|0 - y\|$
62	61	3expa	$⊢ ((φ \land S D Y = S \times \{0\}) \land (φ \land y \in S)) \to \|Y (0) - Y (y)\| \leq 0 \cdot \|0 - y\|$
63	62	3impdi	$⊢ (φ \land S D Y = S \times \{0\} \land y \in S) \to \|Y (0) - Y (y)\| \leq 0 \cdot \|0 - y\|$
64		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
65	1 64	syl	$⊢ φ \to S \subseteq ℂ$
66	65	sseld	$⊢ φ \to (y \in S \to y \in ℂ)$
67		subcl	$⊢ (0 \in ℂ \land y \in ℂ) \to 0 - y \in ℂ$
68	67	abscld	$⊢ (0 \in ℂ \land y \in ℂ) \to \|0 - y\| \in ℝ$
69	9 68	mpan	$⊢ y \in ℂ \to \|0 - y\| \in ℝ$
70	66 69	syl6	$⊢ φ \to (y \in S \to \|0 - y\| \in ℝ)$
71	70	imp	$⊢ (φ \land y \in S) \to \|0 - y\| \in ℝ$
72	71	recnd	$⊢ (φ \land y \in S) \to \|0 - y\| \in ℂ$
73	72	mul02d	$⊢ (φ \land y \in S) \to 0 \cdot \|0 - y\| = 0$
74	73	3adant2	$⊢ (φ \land S D Y = S \times \{0\} \land y \in S) \to 0 \cdot \|0 - y\| = 0$
75	63 74	breqtrd	$⊢ (φ \land S D Y = S \times \{0\} \land y \in S) \to \|Y (0) - Y (y)\| \leq 0$
76		ffvelcdm	$⊢ (Y : S ⟶ ℂ \land y \in S) \to Y (y) \in ℂ$
77	14 76	anim12dan	$⊢ (Y : S ⟶ ℂ \land (0 \in S \land y \in S)) \to (Y (0) \in ℂ \land Y (y) \in ℂ)$
78	2 77	sylan	$⊢ (φ \land (0 \in S \land y \in S)) \to (Y (0) \in ℂ \land Y (y) \in ℂ)$
79	78	3impb	$⊢ (φ \land 0 \in S \land y \in S) \to (Y (0) \in ℂ \land Y (y) \in ℂ)$
80	13 79	syl3an2	$⊢ (φ \land φ \land y \in S) \to (Y (0) \in ℂ \land Y (y) \in ℂ)$
81	80	3anidm12	$⊢ (φ \land y \in S) \to (Y (0) \in ℂ \land Y (y) \in ℂ)$
82		subcl	$⊢ (Y (0) \in ℂ \land Y (y) \in ℂ) \to Y (0) - Y (y) \in ℂ$
83	81 82	syl	$⊢ (φ \land y \in S) \to Y (0) - Y (y) \in ℂ$
84	83	absge0d	$⊢ (φ \land y \in S) \to 0 \leq \|Y (0) - Y (y)\|$
85	84	3adant2	$⊢ (φ \land S D Y = S \times \{0\} \land y \in S) \to 0 \leq \|Y (0) - Y (y)\|$
86	83	abscld	$⊢ (φ \land y \in S) \to \|Y (0) - Y (y)\| \in ℝ$
87		letri3	$⊢ (\|Y (0) - Y (y)\| \in ℝ \land 0 \in ℝ) \to (\|Y (0) - Y (y)\| = 0 \leftrightarrow (\|Y (0) - Y (y)\| \leq 0 \land 0 \leq \|Y (0) - Y (y)\|))$
88	86 6 87	sylancl	$⊢ (φ \land y \in S) \to (\|Y (0) - Y (y)\| = 0 \leftrightarrow (\|Y (0) - Y (y)\| \leq 0 \land 0 \leq \|Y (0) - Y (y)\|))$
89	88	3adant2	$⊢ (φ \land S D Y = S \times \{0\} \land y \in S) \to (\|Y (0) - Y (y)\| = 0 \leftrightarrow (\|Y (0) - Y (y)\| \leq 0 \land 0 \leq \|Y (0) - Y (y)\|))$
90	75 85 89	mpbir2and	$⊢ (φ \land S D Y = S \times \{0\} \land y \in S) \to \|Y (0) - Y (y)\| = 0$
91	83	abs00ad	$⊢ (φ \land y \in S) \to (\|Y (0) - Y (y)\| = 0 \leftrightarrow Y (0) - Y (y) = 0)$
92	91	3adant2	$⊢ (φ \land S D Y = S \times \{0\} \land y \in S) \to (\|Y (0) - Y (y)\| = 0 \leftrightarrow Y (0) - Y (y) = 0)$
93	90 92	mpbid	$⊢ (φ \land S D Y = S \times \{0\} \land y \in S) \to Y (0) - Y (y) = 0$
94		subeq0	$⊢ (Y (0) \in ℂ \land Y (y) \in ℂ) \to (Y (0) - Y (y) = 0 \leftrightarrow Y (0) = Y (y))$
95	81 94	syl	$⊢ (φ \land y \in S) \to (Y (0) - Y (y) = 0 \leftrightarrow Y (0) = Y (y))$
96	95	3adant2	$⊢ (φ \land S D Y = S \times \{0\} \land y \in S) \to (Y (0) - Y (y) = 0 \leftrightarrow Y (0) = Y (y))$
97	93 96	mpbid	$⊢ (φ \land S D Y = S \times \{0\} \land y \in S) \to Y (0) = Y (y)$
98	97	3expa	$⊢ ((φ \land S D Y = S \times \{0\}) \land y \in S) \to Y (0) = Y (y)$
99	23 98	eqtr2d	$⊢ ((φ \land S D Y = S \times \{0\}) \land y \in S) \to Y (y) = (S \times \{Y (0)\}) (y)$
100	18 21 99	eqfnfvd	$⊢ (φ \land S D Y = S \times \{0\}) \to Y = S \times \{Y (0)\}$
101		sneq	$⊢ x = Y (0) \to \{x\} = \{Y (0)\}$
102	101	xpeq2d	$⊢ x = Y (0) \to S \times \{x\} = S \times \{Y (0)\}$
103	102	rspceeqv	$⊢ (Y (0) \in ℂ \land Y = S \times \{Y (0)\}) \to \exists x \in ℂ Y = S \times \{x\}$
104	16 100 103	syl2anc	$⊢ (φ \land S D Y = S \times \{0\}) \to \exists x \in ℂ Y = S \times \{x\}$
105	104	ex	$⊢ φ \to (S D Y = S \times \{0\} \to \exists x \in ℂ Y = S \times \{x\})$
106		oveq2	$⊢ Y = S \times \{x\} \to S D Y = S D (S \times \{x\})$
107	106	3ad2ant3	$⊢ (φ \land x \in ℂ \land Y = S \times \{x\}) \to S D Y = S D (S \times \{x\})$
108		dvsconst	$⊢ (S \in \{ℝ, ℂ\} \land x \in ℂ) \to S D (S \times \{x\}) = S \times \{0\}$
109	1 108	sylan	$⊢ (φ \land x \in ℂ) \to S D (S \times \{x\}) = S \times \{0\}$
110	109	3adant3	$⊢ (φ \land x \in ℂ \land Y = S \times \{x\}) \to S D (S \times \{x\}) = S \times \{0\}$
111	107 110	eqtrd	$⊢ (φ \land x \in ℂ \land Y = S \times \{x\}) \to S D Y = S \times \{0\}$
112	111	rexlimdv3a	$⊢ φ \to (\exists x \in ℂ Y = S \times \{x\} \to S D Y = S \times \{0\})$
113	105 112	impbid	$⊢ φ \to (S D Y = S \times \{0\} \leftrightarrow \exists x \in ℂ Y = S \times \{x\})$
114		sneq	$⊢ c = x \to \{c\} = \{x\}$
115	114	xpeq2d	$⊢ c = x \to S \times \{c\} = S \times \{x\}$
116	115	eqeq2d	$⊢ c = x \to (Y = S \times \{c\} \leftrightarrow Y = S \times \{x\})$
117	116	cbvrexvw	$⊢ \exists c \in ℂ Y = S \times \{c\} \leftrightarrow \exists x \in ℂ Y = S \times \{x\}$
118	113 117	bitr4di	$⊢ φ \to (S D Y = S \times \{0\} \leftrightarrow \exists c \in ℂ Y = S \times \{c\})$

Metamath Proof Explorer

Theorem dvconstbi

Proof