dvfval

Description: Value and set bounds on the derivative operator. (Contributed by Mario Carneiro, 7-Aug-2014) (Revised by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Hypotheses	dvval.t	$⊢ T = K ↾_{𝑡} S$
	dvval.k	$⊢ K = TopOpen (ℂ_{fld})$
Assertion	dvfval	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to (S D F = ⋃_{x \in int (T) (A)} (\{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)) \land S D F \subseteq int (T) (A) \times ℂ)$

Proof

Step	Hyp	Ref	Expression
1		dvval.t	$⊢ T = K ↾_{𝑡} S$
2		dvval.k	$⊢ K = TopOpen (ℂ_{fld})$
3		df-dv	$⊢ D = (s \in 𝒫 ℂ, f \in (ℂ ↑_{𝑝𝑚} s) ⟼ ⋃_{x \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} s) (dom f)} (\{x\} \times ((z \in (dom f ∖ \{x\}) ⟼ \frac{f (z) - f (x)}{z - x}) {lim}_{ℂ} x)))$
4	3	a1i	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to D = (s \in 𝒫 ℂ, f \in (ℂ ↑_{𝑝𝑚} s) ⟼ ⋃_{x \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} s) (dom f)} (\{x\} \times ((z \in (dom f ∖ \{x\}) ⟼ \frac{f (z) - f (x)}{z - x}) {lim}_{ℂ} x)))$
5	2	oveq1i	$⊢ K ↾_{𝑡} s = TopOpen (ℂ_{fld}) ↾_{𝑡} s$
6		simprl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to s = S$
7	6	oveq2d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to K ↾_{𝑡} s = K ↾_{𝑡} S$
8	7 1	eqtr4di	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to K ↾_{𝑡} s = T$
9	5 8	eqtr3id	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} s = T$
10	9	fveq2d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} s) = int (T)$
11		simprr	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to f = F$
12	11	dmeqd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to dom f = dom F$
13		simpl2	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to F : A ⟶ ℂ$
14	13	fdmd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to dom F = A$
15	12 14	eqtrd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to dom f = A$
16	10 15	fveq12d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} s) (dom f) = int (T) (A)$
17	15	difeq1d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to dom f ∖ \{x\} = A ∖ \{x\}$
18	11	fveq1d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to f (z) = F (z)$
19	11	fveq1d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to f (x) = F (x)$
20	18 19	oveq12d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to f (z) - f (x) = F (z) - F (x)$
21	20	oveq1d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to \frac{f (z) - f (x)}{z - x} = \frac{F (z) - F (x)}{z - x}$
22	17 21	mpteq12dv	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to (z \in (dom f ∖ \{x\}) ⟼ \frac{f (z) - f (x)}{z - x}) = (z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
23	22	oveq1d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to (z \in (dom f ∖ \{x\}) ⟼ \frac{f (z) - f (x)}{z - x}) {lim}_{ℂ} x = (z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x$
24	23	xpeq2d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to \{x\} \times ((z \in (dom f ∖ \{x\}) ⟼ \frac{f (z) - f (x)}{z - x}) {lim}_{ℂ} x) = \{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)$
25	16 24	iuneq12d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land (s = S \land f = F)) \to ⋃_{x \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} s) (dom f)} (\{x\} \times ((z \in (dom f ∖ \{x\}) ⟼ \frac{f (z) - f (x)}{z - x}) {lim}_{ℂ} x)) = ⋃_{x \in int (T) (A)} (\{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x))$
26		simpr	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land s = S) \to s = S$
27	26	oveq2d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land s = S) \to ℂ ↑_{𝑝𝑚} s = ℂ ↑_{𝑝𝑚} S$
28		simp1	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to S \subseteq ℂ$
29		cnex	$⊢ ℂ \in V$
30	29	elpw2	$⊢ S \in 𝒫 ℂ \leftrightarrow S \subseteq ℂ$
31	28 30	sylibr	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to S \in 𝒫 ℂ$
32	29	a1i	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to ℂ \in V$
33		simp2	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to F : A ⟶ ℂ$
34		simp3	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to A \subseteq S$
35		elpm2r	$⊢ ((ℂ \in V \land S \in 𝒫 ℂ) \land (F : A ⟶ ℂ \land A \subseteq S)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
36	32 31 33 34 35	syl22anc	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to F \in (ℂ ↑_{𝑝𝑚} S)$
37		limccl	$⊢ (z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x \subseteq ℂ$
38		xpss2	$⊢ (z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x \subseteq ℂ \to \{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x) \subseteq \{x\} \times ℂ$
39	37 38	ax-mp	$⊢ \{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x) \subseteq \{x\} \times ℂ$
40	39	rgenw	$⊢ \forall x \in int (T) (A) \{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x) \subseteq \{x\} \times ℂ$
41		ss2iun	$⊢ \forall x \in int (T) (A) \{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x) \subseteq \{x\} \times ℂ \to ⋃_{x \in int (T) (A)} (\{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)) \subseteq ⋃_{x \in int (T) (A)} (\{x\} \times ℂ)$
42	40 41	ax-mp	$⊢ ⋃_{x \in int (T) (A)} (\{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)) \subseteq ⋃_{x \in int (T) (A)} (\{x\} \times ℂ)$
43		iunxpconst	$⊢ ⋃_{x \in int (T) (A)} (\{x\} \times ℂ) = int (T) (A) \times ℂ$
44	42 43	sseqtri	$⊢ ⋃_{x \in int (T) (A)} (\{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)) \subseteq int (T) (A) \times ℂ$
45	44	a1i	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to ⋃_{x \in int (T) (A)} (\{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)) \subseteq int (T) (A) \times ℂ$
46		fvex	$⊢ int (T) (A) \in V$
47	46 29	xpex	$⊢ int (T) (A) \times ℂ \in V$
48	47	ssex	$⊢ ⋃_{x \in int (T) (A)} (\{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)) \subseteq int (T) (A) \times ℂ \to ⋃_{x \in int (T) (A)} (\{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)) \in V$
49	45 48	syl	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to ⋃_{x \in int (T) (A)} (\{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)) \in V$
50	4 25 27 31 36 49	ovmpodx	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to S D F = ⋃_{x \in int (T) (A)} (\{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x))$
51	50 45	eqsstrd	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to S D F \subseteq int (T) (A) \times ℂ$
52	50 51	jca	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to (S D F = ⋃_{x \in int (T) (A)} (\{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)) \land S D F \subseteq int (T) (A) \times ℂ)$

Metamath Proof Explorer

Theorem dvfval

Proof