perfdvf

Description: The derivative is a function, whenever it is defined relative to a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 25-Dec-2016)

		Ref	Expression
	Hypothesis	perfdvf.1	$⊢ K = TopOpen (ℂ_{fld})$
	Assertion	perfdvf	$⊢ K ↾_{𝑡} S \in Perf \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$

Proof

Step	Hyp	Ref	Expression
1		perfdvf.1	$⊢ K = TopOpen (ℂ_{fld})$
2		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)))$
3	2	dmmpossx	$⊢ dom D \subseteq ⋃_{s \in 𝒫 ℂ} (\{s\} \times (ℂ ↑_{𝑝𝑚} s))$
4		simpl	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to ⟨S, F⟩ \in dom D$
5	3 4	sseldi	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to ⟨S, F⟩ \in ⋃_{s \in 𝒫 ℂ} (\{s\} \times (ℂ ↑_{𝑝𝑚} s))$
6		oveq2	$⊢ s = S \to ℂ ↑_{𝑝𝑚} s = ℂ ↑_{𝑝𝑚} S$
7	6	opeliunxp2	$⊢ ⟨S, F⟩ \in ⋃_{s \in 𝒫 ℂ} (\{s\} \times (ℂ ↑_{𝑝𝑚} s)) \leftrightarrow (S \in 𝒫 ℂ \land F \in (ℂ ↑_{𝑝𝑚} S))$
8	5 7	sylib	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to (S \in 𝒫 ℂ \land F \in (ℂ ↑_{𝑝𝑚} S))$
9	8	simprd	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to F \in (ℂ ↑_{𝑝𝑚} S)$
10		cnex	$⊢ ℂ \in V$
11	8	simpld	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to S \in 𝒫 ℂ$
12		elpm2g	$⊢ (ℂ \in V \land S \in 𝒫 ℂ) \to (F \in (ℂ ↑_{𝑝𝑚} S) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq S))$
13	10 11 12	sylancr	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to (F \in (ℂ ↑_{𝑝𝑚} S) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq S))$
14	9 13	mpbid	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to (F : dom F ⟶ ℂ \land dom F \subseteq S)$
15	14	simpld	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to F : dom F ⟶ ℂ$
16	15	adantr	$⊢ ((⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \land x \in int (K ↾_{𝑡} S) (dom F)) \to F : dom F ⟶ ℂ$
17	3	sseli	$⊢ ⟨S, F⟩ \in dom D \to ⟨S, F⟩ \in ⋃_{s \in 𝒫 ℂ} (\{s\} \times (ℂ ↑_{𝑝𝑚} s))$
18	17 7	sylib	$⊢ ⟨S, F⟩ \in dom D \to (S \in 𝒫 ℂ \land F \in (ℂ ↑_{𝑝𝑚} S))$
19	18	simprd	$⊢ ⟨S, F⟩ \in dom D \to F \in (ℂ ↑_{𝑝𝑚} S)$
20	18	simpld	$⊢ ⟨S, F⟩ \in dom D \to S \in 𝒫 ℂ$
21	10 20 12	sylancr	$⊢ ⟨S, F⟩ \in dom D \to (F \in (ℂ ↑_{𝑝𝑚} S) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq S))$
22	19 21	mpbid	$⊢ ⟨S, F⟩ \in dom D \to (F : dom F ⟶ ℂ \land dom F \subseteq S)$
23	22	simprd	$⊢ ⟨S, F⟩ \in dom D \to dom F \subseteq S$
24	23	adantr	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to dom F \subseteq S$
25	11	elpwid	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to S \subseteq ℂ$
26	24 25	sstrd	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to dom F \subseteq ℂ$
27	26	adantr	$⊢ ((⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \land x \in int (K ↾_{𝑡} S) (dom F)) \to dom F \subseteq ℂ$
28	1	cnfldtopon	$⊢ K \in TopOn (ℂ)$
29		resttopon	$⊢ (K \in TopOn (ℂ) \land S \subseteq ℂ) \to K ↾_{𝑡} S \in TopOn (S)$
30	28 25 29	sylancr	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to K ↾_{𝑡} S \in TopOn (S)$
31		topontop	$⊢ K ↾_{𝑡} S \in TopOn (S) \to K ↾_{𝑡} S \in Top$
32	30 31	syl	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to K ↾_{𝑡} S \in Top$
33		toponuni	$⊢ K ↾_{𝑡} S \in TopOn (S) \to S = ⋃ (K ↾_{𝑡} S)$
34	30 33	syl	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to S = ⋃ (K ↾_{𝑡} S)$
35	24 34	sseqtrd	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to dom F \subseteq ⋃ (K ↾_{𝑡} S)$
36		eqid	$⊢ ⋃ (K ↾_{𝑡} S) = ⋃ (K ↾_{𝑡} S)$
37	36	ntrss2	$⊢ (K ↾_{𝑡} S \in Top \land dom F \subseteq ⋃ (K ↾_{𝑡} S)) \to int (K ↾_{𝑡} S) (dom F) \subseteq dom F$
38	32 35 37	syl2anc	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to int (K ↾_{𝑡} S) (dom F) \subseteq dom F$
39	38	sselda	$⊢ ((⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \land x \in int (K ↾_{𝑡} S) (dom F)) \to x \in dom F$
40	16 27 39	dvlem	$⊢ (((⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \land x \in int (K ↾_{𝑡} S) (dom F)) \land z \in (dom F ∖ \{x\})) \to \frac{F (z) - F (x)}{z - x} \in ℂ$
41	40	fmpttd	$⊢ ((⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \land x \in int (K ↾_{𝑡} S) (dom F)) \to (z \in (dom F ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) : dom F ∖ \{x\} ⟶ ℂ$
42	27	ssdifssd	$⊢ ((⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \land x \in int (K ↾_{𝑡} S) (dom F)) \to dom F ∖ \{x\} \subseteq ℂ$
43	36	ntrss3	$⊢ (K ↾_{𝑡} S \in Top \land dom F \subseteq ⋃ (K ↾_{𝑡} S)) \to int (K ↾_{𝑡} S) (dom F) \subseteq ⋃ (K ↾_{𝑡} S)$
44	32 35 43	syl2anc	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to int (K ↾_{𝑡} S) (dom F) \subseteq ⋃ (K ↾_{𝑡} S)$
45	44 34	sseqtrrd	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to int (K ↾_{𝑡} S) (dom F) \subseteq S$
46		restabs	$⊢ (K \in TopOn (ℂ) \land int (K ↾_{𝑡} S) (dom F) \subseteq S \land S \in 𝒫 ℂ) \to (K ↾_{𝑡} S) ↾_{𝑡} int (K ↾_{𝑡} S) (dom F) = K ↾_{𝑡} int (K ↾_{𝑡} S) (dom F)$
47	28 45 11 46	mp3an2i	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to (K ↾_{𝑡} S) ↾_{𝑡} int (K ↾_{𝑡} S) (dom F) = K ↾_{𝑡} int (K ↾_{𝑡} S) (dom F)$
48		simpr	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to K ↾_{𝑡} S \in Perf$
49	36	ntropn	$⊢ (K ↾_{𝑡} S \in Top \land dom F \subseteq ⋃ (K ↾_{𝑡} S)) \to int (K ↾_{𝑡} S) (dom F) \in (K ↾_{𝑡} S)$
50	32 35 49	syl2anc	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to int (K ↾_{𝑡} S) (dom F) \in (K ↾_{𝑡} S)$
51		eqid	$⊢ (K ↾_{𝑡} S) ↾_{𝑡} int (K ↾_{𝑡} S) (dom F) = (K ↾_{𝑡} S) ↾_{𝑡} int (K ↾_{𝑡} S) (dom F)$
52	36 51	perfopn	$⊢ (K ↾_{𝑡} S \in Perf \land int (K ↾_{𝑡} S) (dom F) \in (K ↾_{𝑡} S)) \to (K ↾_{𝑡} S) ↾_{𝑡} int (K ↾_{𝑡} S) (dom F) \in Perf$
53	48 50 52	syl2anc	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to (K ↾_{𝑡} S) ↾_{𝑡} int (K ↾_{𝑡} S) (dom F) \in Perf$
54	47 53	eqeltrrd	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to K ↾_{𝑡} int (K ↾_{𝑡} S) (dom F) \in Perf$
55	1	cnfldtop	$⊢ K \in Top$
56	45 25	sstrd	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to int (K ↾_{𝑡} S) (dom F) \subseteq ℂ$
57	28	toponunii	$⊢ ℂ = ⋃ K$
58		eqid	$⊢ K ↾_{𝑡} int (K ↾_{𝑡} S) (dom F) = K ↾_{𝑡} int (K ↾_{𝑡} S) (dom F)$
59	57 58	restperf	$⊢ (K \in Top \land int (K ↾_{𝑡} S) (dom F) \subseteq ℂ) \to (K ↾_{𝑡} int (K ↾_{𝑡} S) (dom F) \in Perf \leftrightarrow int (K ↾_{𝑡} S) (dom F) \subseteq limPt (K) (int (K ↾_{𝑡} S) (dom F)))$
60	55 56 59	sylancr	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to (K ↾_{𝑡} int (K ↾_{𝑡} S) (dom F) \in Perf \leftrightarrow int (K ↾_{𝑡} S) (dom F) \subseteq limPt (K) (int (K ↾_{𝑡} S) (dom F)))$
61	54 60	mpbid	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to int (K ↾_{𝑡} S) (dom F) \subseteq limPt (K) (int (K ↾_{𝑡} S) (dom F))$
62	57	lpss3	$⊢ (K \in Top \land dom F \subseteq ℂ \land int (K ↾_{𝑡} S) (dom F) \subseteq dom F) \to limPt (K) (int (K ↾_{𝑡} S) (dom F)) \subseteq limPt (K) (dom F)$
63	55 26 38 62	mp3an2i	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to limPt (K) (int (K ↾_{𝑡} S) (dom F)) \subseteq limPt (K) (dom F)$
64	61 63	sstrd	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to int (K ↾_{𝑡} S) (dom F) \subseteq limPt (K) (dom F)$
65	64	sselda	$⊢ ((⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \land x \in int (K ↾_{𝑡} S) (dom F)) \to x \in limPt (K) (dom F)$
66	57	lpdifsn	$⊢ (K \in Top \land dom F \subseteq ℂ) \to (x \in limPt (K) (dom F) \leftrightarrow x \in limPt (K) (dom F ∖ \{x\}))$
67	55 27 66	sylancr	$⊢ ((⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \land x \in int (K ↾_{𝑡} S) (dom F)) \to (x \in limPt (K) (dom F) \leftrightarrow x \in limPt (K) (dom F ∖ \{x\}))$
68	65 67	mpbid	$⊢ ((⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \land x \in int (K ↾_{𝑡} S) (dom F)) \to x \in limPt (K) (dom F ∖ \{x\})$
69	41 42 68 1	limcmo	$⊢ ((⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \land x \in int (K ↾_{𝑡} S) (dom F)) \to \exists^{*} y y \in ((z \in (dom F ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)$
70	69	ex	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to (x \in int (K ↾_{𝑡} S) (dom F) \to \exists^{*} y y \in ((z \in (dom F ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x))$
71		moanimv	$⊢ \exists^{} y (x \in int (K ↾_{𝑡} S) (dom F) \land y \in ((z \in (dom F ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)) \leftrightarrow (x \in int (K ↾_{𝑡} S) (dom F) \to \exists^{} y y \in ((z \in (dom F ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x))$
72	70 71	sylibr	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to \exists^{*} y (x \in int (K ↾_{𝑡} S) (dom F) \land y \in ((z \in (dom F ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x))$
73		eqid	$⊢ K ↾_{𝑡} S = K ↾_{𝑡} S$
74		eqid	$⊢ (z \in (dom F ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) = (z \in (dom F ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
75	73 1 74 25 15 24	eldv	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to (x F_{S}^{'} y \leftrightarrow (x \in int (K ↾_{𝑡} S) (dom F) \land y \in ((z \in (dom F ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)))$
76	75	mobidv	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to (\exists^{} y x F_{S}^{'} y \leftrightarrow \exists^{} y (x \in int (K ↾_{𝑡} S) (dom F) \land y \in ((z \in (dom F ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)))$
77	72 76	mpbird	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to \exists^{*} y x F_{S}^{'} y$
78	77	alrimiv	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to \forall x \exists^{*} y x F_{S}^{'} y$
79		reldv	$⊢ Rel F_{S}^{'}$
80		dffun6	$⊢ Fun F_{S}^{'} \leftrightarrow (Rel F_{S}^{'} \land \forall x \exists^{*} y x F_{S}^{'} y)$
81	79 80	mpbiran	$⊢ Fun F_{S}^{'} \leftrightarrow \forall x \exists^{*} y x F_{S}^{'} y$
82	78 81	sylibr	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to Fun F_{S}^{'}$
83	82	funfnd	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to F_{S}^{'} Fn dom F_{S}^{'}$
84		vex	$⊢ y \in V$
85	84	elrn	$⊢ y \in ran F_{S}^{'} \leftrightarrow \exists x x F_{S}^{'} y$
86	25 15 24	dvcl	$⊢ ((⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \land x F_{S}^{'} y) \to y \in ℂ$
87	86	ex	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to (x F_{S}^{'} y \to y \in ℂ)$
88	87	exlimdv	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to (\exists x x F_{S}^{'} y \to y \in ℂ)$
89	85 88	syl5bi	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to (y \in ran F_{S}^{'} \to y \in ℂ)$
90	89	ssrdv	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to ran F_{S}^{'} \subseteq ℂ$
91		df-f	$⊢ F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \leftrightarrow (F_{S}^{'} Fn dom F_{S}^{'} \land ran F_{S}^{'} \subseteq ℂ)$
92	83 90 91	sylanbrc	$⊢ (⟨S, F⟩ \in dom D \land K ↾_{𝑡} S \in Perf) \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
93	92	ex	$⊢ ⟨S, F⟩ \in dom D \to (K ↾_{𝑡} S \in Perf \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ)$
94		f0	$⊢ \emptyset : \emptyset ⟶ ℂ$
95		df-ov	$⊢ S D F = D (⟨S, F⟩)$
96		ndmfv	$⊢ \neg ⟨S, F⟩ \in dom D \to D (⟨S, F⟩) = \emptyset$
97	95 96	syl5eq	$⊢ \neg ⟨S, F⟩ \in dom D \to S D F = \emptyset$
98	97	dmeqd	$⊢ \neg ⟨S, F⟩ \in dom D \to dom F_{S}^{'} = dom \emptyset$
99		dm0	$⊢ dom \emptyset = \emptyset$
100	98 99	eqtrdi	$⊢ \neg ⟨S, F⟩ \in dom D \to dom F_{S}^{'} = \emptyset$
101	97 100	feq12d	$⊢ \neg ⟨S, F⟩ \in dom D \to (F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \leftrightarrow \emptyset : \emptyset ⟶ ℂ)$
102	94 101	mpbiri	$⊢ \neg ⟨S, F⟩ \in dom D \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
103	102	a1d	$⊢ \neg ⟨S, F⟩ \in dom D \to (K ↾_{𝑡} S \in Perf \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ)$
104	93 103	pm2.61i	$⊢ K ↾_{𝑡} S \in Perf \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$

Metamath Proof Explorer

Theorem perfdvf

Proof