dvres2lem

	Ref	Expression
Hypotheses	dvres.k	$⊢ K = TopOpen (ℂ_{fld})$
	dvres.t	$⊢ T = K ↾_{𝑡} S$
	dvres.g	$⊢ G = (z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
	dvres.s	$⊢ φ \to S \subseteq ℂ$
	dvres.f	$⊢ φ \to F : A ⟶ ℂ$
	dvres.a	$⊢ φ \to A \subseteq S$
	dvres.b	$⊢ φ \to B \subseteq S$
	dvres.y	$⊢ φ \to y \in ℂ$
	dvres2lem.d	$⊢ φ \to x F_{S}^{'} y$
	dvres2lem.x	$⊢ φ \to x \in B$
Assertion	dvres2lem	$⊢ φ \to x {({F ↾}_{B})}_{B}^{'} y$

Proof

Step	Hyp	Ref	Expression
1		dvres.k	$⊢ K = TopOpen (ℂ_{fld})$
2		dvres.t	$⊢ T = K ↾_{𝑡} S$
3		dvres.g	$⊢ G = (z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
4		dvres.s	$⊢ φ \to S \subseteq ℂ$
5		dvres.f	$⊢ φ \to F : A ⟶ ℂ$
6		dvres.a	$⊢ φ \to A \subseteq S$
7		dvres.b	$⊢ φ \to B \subseteq S$
8		dvres.y	$⊢ φ \to y \in ℂ$
9		dvres2lem.d	$⊢ φ \to x F_{S}^{'} y$
10		dvres2lem.x	$⊢ φ \to x \in B$
11	1	cnfldtop	$⊢ K \in Top$
12		cnex	$⊢ ℂ \in V$
13		ssexg	$⊢ (S \subseteq ℂ \land ℂ \in V) \to S \in V$
14	4 12 13	sylancl	$⊢ φ \to S \in V$
15		resttop	$⊢ (K \in Top \land S \in V) \to K ↾_{𝑡} S \in Top$
16	11 14 15	sylancr	$⊢ φ \to K ↾_{𝑡} S \in Top$
17	2 16	eqeltrid	$⊢ φ \to T \in Top$
18		inss1	$⊢ A \cap B \subseteq A$
19	18 6	sstrid	$⊢ φ \to A \cap B \subseteq S$
20	1	cnfldtopon	$⊢ K \in TopOn (ℂ)$
21		resttopon	$⊢ (K \in TopOn (ℂ) \land S \subseteq ℂ) \to K ↾_{𝑡} S \in TopOn (S)$
22	20 4 21	sylancr	$⊢ φ \to K ↾_{𝑡} S \in TopOn (S)$
23	2 22	eqeltrid	$⊢ φ \to T \in TopOn (S)$
24		toponuni	$⊢ T \in TopOn (S) \to S = ⋃ T$
25	23 24	syl	$⊢ φ \to S = ⋃ T$
26	19 25	sseqtrd	$⊢ φ \to A \cap B \subseteq ⋃ T$
27		difssd	$⊢ φ \to ⋃ T ∖ B \subseteq ⋃ T$
28	26 27	unssd	$⊢ φ \to (A \cap B) \cup (⋃ T ∖ B) \subseteq ⋃ T$
29		inundif	$⊢ (A \cap B) \cup (A ∖ B) = A$
30	6 25	sseqtrd	$⊢ φ \to A \subseteq ⋃ T$
31		ssdif	$⊢ A \subseteq ⋃ T \to A ∖ B \subseteq ⋃ T ∖ B$
32		unss2	$⊢ A ∖ B \subseteq ⋃ T ∖ B \to (A \cap B) \cup (A ∖ B) \subseteq (A \cap B) \cup (⋃ T ∖ B)$
33	30 31 32	3syl	$⊢ φ \to (A \cap B) \cup (A ∖ B) \subseteq (A \cap B) \cup (⋃ T ∖ B)$
34	29 33	eqsstrrid	$⊢ φ \to A \subseteq (A \cap B) \cup (⋃ T ∖ B)$
35		eqid	$⊢ ⋃ T = ⋃ T$
36	35	ntrss	$⊢ (T \in Top \land (A \cap B) \cup (⋃ T ∖ B) \subseteq ⋃ T \land A \subseteq (A \cap B) \cup (⋃ T ∖ B)) \to int (T) (A) \subseteq int (T) ((A \cap B) \cup (⋃ T ∖ B))$
37	17 28 34 36	syl3anc	$⊢ φ \to int (T) (A) \subseteq int (T) ((A \cap B) \cup (⋃ T ∖ B))$
38	2 1 3 4 5 6	eldv	$⊢ φ \to (x F_{S}^{'} y \leftrightarrow (x \in int (T) (A) \land y \in (G {lim}_{ℂ} x)))$
39	9 38	mpbid	$⊢ φ \to (x \in int (T) (A) \land y \in (G {lim}_{ℂ} x))$
40	39	simpld	$⊢ φ \to x \in int (T) (A)$
41	37 40	sseldd	$⊢ φ \to x \in int (T) ((A \cap B) \cup (⋃ T ∖ B))$
42	41 10	elind	$⊢ φ \to x \in (int (T) ((A \cap B) \cup (⋃ T ∖ B)) \cap B)$
43	7 25	sseqtrd	$⊢ φ \to B \subseteq ⋃ T$
44		inss2	$⊢ A \cap B \subseteq B$
45	44	a1i	$⊢ φ \to A \cap B \subseteq B$
46		eqid	$⊢ T ↾_{𝑡} B = T ↾_{𝑡} B$
47	35 46	restntr	$⊢ (T \in Top \land B \subseteq ⋃ T \land A \cap B \subseteq B) \to int (T ↾_{𝑡} B) (A \cap B) = int (T) ((A \cap B) \cup (⋃ T ∖ B)) \cap B$
48	17 43 45 47	syl3anc	$⊢ φ \to int (T ↾_{𝑡} B) (A \cap B) = int (T) ((A \cap B) \cup (⋃ T ∖ B)) \cap B$
49	2	oveq1i	$⊢ T ↾_{𝑡} B = (K ↾_{𝑡} S) ↾_{𝑡} B$
50	11	a1i	$⊢ φ \to K \in Top$
51		restabs	$⊢ (K \in Top \land B \subseteq S \land S \in V) \to (K ↾_{𝑡} S) ↾_{𝑡} B = K ↾_{𝑡} B$
52	50 7 14 51	syl3anc	$⊢ φ \to (K ↾_{𝑡} S) ↾_{𝑡} B = K ↾_{𝑡} B$
53	49 52	eqtrid	$⊢ φ \to T ↾_{𝑡} B = K ↾_{𝑡} B$
54	53	fveq2d	$⊢ φ \to int (T ↾_{𝑡} B) = int (K ↾_{𝑡} B)$
55	54	fveq1d	$⊢ φ \to int (T ↾_{𝑡} B) (A \cap B) = int (K ↾_{𝑡} B) (A \cap B)$
56	48 55	eqtr3d	$⊢ φ \to int (T) ((A \cap B) \cup (⋃ T ∖ B)) \cap B = int (K ↾_{𝑡} B) (A \cap B)$
57	42 56	eleqtrd	$⊢ φ \to x \in int (K ↾_{𝑡} B) (A \cap B)$
58		limcresi	$⊢ G {lim}_{ℂ} x \subseteq ({G ↾}_{((A \cap B) ∖ \{x\})}) {lim}_{ℂ} x$
59	39	simprd	$⊢ φ \to y \in (G {lim}_{ℂ} x)$
60	58 59	sselid	$⊢ φ \to y \in (({G ↾}_{((A \cap B) ∖ \{x\})}) {lim}_{ℂ} x)$
61		difss	$⊢ (A \cap B) ∖ \{x\} \subseteq A \cap B$
62	61 44	sstri	$⊢ (A \cap B) ∖ \{x\} \subseteq B$
63	62	sseli	$⊢ z \in ((A \cap B) ∖ \{x\}) \to z \in B$
64		fvres	$⊢ z \in B \to ({F ↾}_{B}) (z) = F (z)$
65	10	fvresd	$⊢ φ \to ({F ↾}_{B}) (x) = F (x)$
66	64 65	oveqan12rd	$⊢ (φ \land z \in B) \to ({F ↾}_{B}) (z) - ({F ↾}_{B}) (x) = F (z) - F (x)$
67	66	oveq1d	$⊢ (φ \land z \in B) \to \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x} = \frac{F (z) - F (x)}{z - x}$
68	63 67	sylan2	$⊢ (φ \land z \in ((A \cap B) ∖ \{x\})) \to \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x} = \frac{F (z) - F (x)}{z - x}$
69	68	mpteq2dva	$⊢ φ \to (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) = (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
70	3	reseq1i	$⊢ {G ↾}_{((A \cap B) ∖ \{x\})} = {(z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) ↾}_{((A \cap B) ∖ \{x\})}$
71		ssdif	$⊢ A \cap B \subseteq A \to (A \cap B) ∖ \{x\} \subseteq A ∖ \{x\}$
72		resmpt	$⊢ (A \cap B) ∖ \{x\} \subseteq A ∖ \{x\} \to {(z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) ↾}_{((A \cap B) ∖ \{x\})} = (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
73	18 71 72	mp2b	$⊢ {(z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) ↾}_{((A \cap B) ∖ \{x\})} = (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
74	70 73	eqtri	$⊢ {G ↾}_{((A \cap B) ∖ \{x\})} = (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x})$
75	69 74	eqtr4di	$⊢ φ \to (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) = {G ↾}_{((A \cap B) ∖ \{x\})}$
76	75	oveq1d	$⊢ φ \to (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) {lim}_{ℂ} x = ({G ↾}_{((A \cap B) ∖ \{x\})}) {lim}_{ℂ} x$
77	60 76	eleqtrrd	$⊢ φ \to y \in ((z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) {lim}_{ℂ} x)$
78		eqid	$⊢ K ↾_{𝑡} B = K ↾_{𝑡} B$
79		eqid	$⊢ (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) = (z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x})$
80	7 4	sstrd	$⊢ φ \to B \subseteq ℂ$
81		fresin	$⊢ F : A ⟶ ℂ \to ({F ↾}_{B}) : A \cap B ⟶ ℂ$
82	5 81	syl	$⊢ φ \to ({F ↾}_{B}) : A \cap B ⟶ ℂ$
83	78 1 79 80 82 45	eldv	$⊢ φ \to (x {({F ↾}_{B})}_{B}^{'} y \leftrightarrow (x \in int (K ↾_{𝑡} B) (A \cap B) \land y \in ((z \in ((A \cap B) ∖ \{x\}) ⟼ \frac{({F ↾}_{B}) (z) - ({F ↾}_{B}) (x)}{z - x}) {lim}_{ℂ} x)))$
84	57 77 83	mpbir2and	$⊢ φ \to x {({F ↾}_{B})}_{B}^{'} y$

Metamath Proof Explorer

Theorem dvres2lem

Proof