dvcnvlem

	Ref	Expression
Hypotheses	dvcnv.j	$⊢ J = TopOpen (ℂ_{fld})$
	dvcnv.k	$⊢ K = J ↾_{𝑡} S$
	dvcnv.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvcnv.y	$⊢ φ \to Y \in K$
	dvcnv.f	$⊢ φ \to F : X \underset{1-1 onto}{⟶} Y$
	dvcnv.i	$⊢ φ \to F^{-1} : Y \underset{cn}{⟶} X$
	dvcnv.d	$⊢ φ \to dom F_{S}^{'} = X$
	dvcnv.z	$⊢ φ \to \neg 0 \in ran F_{S}^{'}$
	dvcnv.c	$⊢ φ \to C \in X$
Assertion	dvcnvlem	$⊢ φ \to F (C) {F^{-1}}_{S}^{'} (\frac{1}{F_{S}^{'} (C)})$

Proof

Step	Hyp	Ref	Expression
1		dvcnv.j	$⊢ J = TopOpen (ℂ_{fld})$
2		dvcnv.k	$⊢ K = J ↾_{𝑡} S$
3		dvcnv.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
4		dvcnv.y	$⊢ φ \to Y \in K$
5		dvcnv.f	$⊢ φ \to F : X \underset{1-1 onto}{⟶} Y$
6		dvcnv.i	$⊢ φ \to F^{-1} : Y \underset{cn}{⟶} X$
7		dvcnv.d	$⊢ φ \to dom F_{S}^{'} = X$
8		dvcnv.z	$⊢ φ \to \neg 0 \in ran F_{S}^{'}$
9		dvcnv.c	$⊢ φ \to C \in X$
10		f1of	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F : X ⟶ Y$
11	5 10	syl	$⊢ φ \to F : X ⟶ Y$
12	11 9	ffvelrnd	$⊢ φ \to F (C) \in Y$
13	1	cnfldtopon	$⊢ J \in TopOn (ℂ)$
14		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
15	3 14	syl	$⊢ φ \to S \subseteq ℂ$
16		resttopon	$⊢ (J \in TopOn (ℂ) \land S \subseteq ℂ) \to J ↾_{𝑡} S \in TopOn (S)$
17	13 15 16	sylancr	$⊢ φ \to J ↾_{𝑡} S \in TopOn (S)$
18	2 17	eqeltrid	$⊢ φ \to K \in TopOn (S)$
19		topontop	$⊢ K \in TopOn (S) \to K \in Top$
20	18 19	syl	$⊢ φ \to K \in Top$
21		isopn3i	$⊢ (K \in Top \land Y \in K) \to int (K) (Y) = Y$
22	20 4 21	syl2anc	$⊢ φ \to int (K) (Y) = Y$
23	12 22	eleqtrrd	$⊢ φ \to F (C) \in int (K) (Y)$
24		f1ocnv	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F^{-1} : Y \underset{1-1 onto}{⟶} X$
25		f1of	$⊢ F^{-1} : Y \underset{1-1 onto}{⟶} X \to F^{-1} : Y ⟶ X$
26	5 24 25	3syl	$⊢ φ \to F^{-1} : Y ⟶ X$
27		eldifi	$⊢ z \in (Y ∖ \{F (C)\}) \to z \in Y$
28		ffvelrn	$⊢ (F^{-1} : Y ⟶ X \land z \in Y) \to F^{-1} (z) \in X$
29	26 27 28	syl2an	$⊢ (φ \land z \in (Y ∖ \{F (C)\})) \to F^{-1} (z) \in X$
30	29	anim1i	$⊢ ((φ \land z \in (Y ∖ \{F (C)\})) \land F^{-1} (z) \neq C) \to (F^{-1} (z) \in X \land F^{-1} (z) \neq C)$
31		eldifsn	$⊢ F^{-1} (z) \in (X ∖ \{C\}) \leftrightarrow (F^{-1} (z) \in X \land F^{-1} (z) \neq C)$
32	30 31	sylibr	$⊢ ((φ \land z \in (Y ∖ \{F (C)\})) \land F^{-1} (z) \neq C) \to F^{-1} (z) \in (X ∖ \{C\})$
33	32	anasss	$⊢ (φ \land (z \in (Y ∖ \{F (C)\}) \land F^{-1} (z) \neq C)) \to F^{-1} (z) \in (X ∖ \{C\})$
34		eldifi	$⊢ y \in (X ∖ \{C\}) \to y \in X$
35		dvbsss	$⊢ dom F_{S}^{'} \subseteq S$
36	7 35	eqsstrrdi	$⊢ φ \to X \subseteq S$
37	36 15	sstrd	$⊢ φ \to X \subseteq ℂ$
38	37	sselda	$⊢ (φ \land y \in X) \to y \in ℂ$
39	34 38	sylan2	$⊢ (φ \land y \in (X ∖ \{C\})) \to y \in ℂ$
40	36 9	sseldd	$⊢ φ \to C \in S$
41	15 40	sseldd	$⊢ φ \to C \in ℂ$
42	41	adantr	$⊢ (φ \land y \in (X ∖ \{C\})) \to C \in ℂ$
43	39 42	subcld	$⊢ (φ \land y \in (X ∖ \{C\})) \to y - C \in ℂ$
44		toponss	$⊢ (K \in TopOn (S) \land Y \in K) \to Y \subseteq S$
45	18 4 44	syl2anc	$⊢ φ \to Y \subseteq S$
46	45 15	sstrd	$⊢ φ \to Y \subseteq ℂ$
47	11 46	fssd	$⊢ φ \to F : X ⟶ ℂ$
48		ffvelrn	$⊢ (F : X ⟶ ℂ \land y \in X) \to F (y) \in ℂ$
49	47 34 48	syl2an	$⊢ (φ \land y \in (X ∖ \{C\})) \to F (y) \in ℂ$
50	46 12	sseldd	$⊢ φ \to F (C) \in ℂ$
51	50	adantr	$⊢ (φ \land y \in (X ∖ \{C\})) \to F (C) \in ℂ$
52	49 51	subcld	$⊢ (φ \land y \in (X ∖ \{C\})) \to F (y) - F (C) \in ℂ$
53		eldifsni	$⊢ y \in (X ∖ \{C\}) \to y \neq C$
54	53	adantl	$⊢ (φ \land y \in (X ∖ \{C\})) \to y \neq C$
55	49 51	subeq0ad	$⊢ (φ \land y \in (X ∖ \{C\})) \to (F (y) - F (C) = 0 \leftrightarrow F (y) = F (C))$
56		f1of1	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F : X \underset{1-1}{⟶} Y$
57	5 56	syl	$⊢ φ \to F : X \underset{1-1}{⟶} Y$
58	57	adantr	$⊢ (φ \land y \in (X ∖ \{C\})) \to F : X \underset{1-1}{⟶} Y$
59	34	adantl	$⊢ (φ \land y \in (X ∖ \{C\})) \to y \in X$
60	9	adantr	$⊢ (φ \land y \in (X ∖ \{C\})) \to C \in X$
61		f1fveq	$⊢ (F : X \underset{1-1}{⟶} Y \land (y \in X \land C \in X)) \to (F (y) = F (C) \leftrightarrow y = C)$
62	58 59 60 61	syl12anc	$⊢ (φ \land y \in (X ∖ \{C\})) \to (F (y) = F (C) \leftrightarrow y = C)$
63	55 62	bitrd	$⊢ (φ \land y \in (X ∖ \{C\})) \to (F (y) - F (C) = 0 \leftrightarrow y = C)$
64	63	necon3bid	$⊢ (φ \land y \in (X ∖ \{C\})) \to (F (y) - F (C) \neq 0 \leftrightarrow y \neq C)$
65	54 64	mpbird	$⊢ (φ \land y \in (X ∖ \{C\})) \to F (y) - F (C) \neq 0$
66	43 52 65	divcld	$⊢ (φ \land y \in (X ∖ \{C\})) \to \frac{y - C}{F (y) - F (C)} \in ℂ$
67		limcresi	$⊢ F^{-1} {lim}_{ℂ} F (C) \subseteq ({F^{-1} ↾}_{(Y ∖ \{F (C)\})}) {lim}_{ℂ} F (C)$
68	26	feqmptd	$⊢ φ \to F^{-1} = (z \in Y ⟼ F^{-1} (z))$
69	68	reseq1d	$⊢ φ \to {F^{-1} ↾}_{(Y ∖ \{F (C)\})} = {(z \in Y ⟼ F^{-1} (z)) ↾}_{(Y ∖ \{F (C)\})}$
70		difss	$⊢ Y ∖ \{F (C)\} \subseteq Y$
71		resmpt	$⊢ Y ∖ \{F (C)\} \subseteq Y \to {(z \in Y ⟼ F^{-1} (z)) ↾}_{(Y ∖ \{F (C)\})} = (z \in (Y ∖ \{F (C)\}) ⟼ F^{-1} (z))$
72	70 71	ax-mp	$⊢ {(z \in Y ⟼ F^{-1} (z)) ↾}_{(Y ∖ \{F (C)\})} = (z \in (Y ∖ \{F (C)\}) ⟼ F^{-1} (z))$
73	69 72	eqtrdi	$⊢ φ \to {F^{-1} ↾}_{(Y ∖ \{F (C)\})} = (z \in (Y ∖ \{F (C)\}) ⟼ F^{-1} (z))$
74	73	oveq1d	$⊢ φ \to ({F^{-1} ↾}_{(Y ∖ \{F (C)\})}) {lim}_{ℂ} F (C) = (z \in (Y ∖ \{F (C)\}) ⟼ F^{-1} (z)) {lim}_{ℂ} F (C)$
75	67 74	sseqtrid	$⊢ φ \to F^{-1} {lim}_{ℂ} F (C) \subseteq (z \in (Y ∖ \{F (C)\}) ⟼ F^{-1} (z)) {lim}_{ℂ} F (C)$
76		f1ocnvfv1	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land C \in X) \to F^{-1} (F (C)) = C$
77	5 9 76	syl2anc	$⊢ φ \to F^{-1} (F (C)) = C$
78	6 12	cnlimci	$⊢ φ \to F^{-1} (F (C)) \in (F^{-1} {lim}_{ℂ} F (C))$
79	77 78	eqeltrrd	$⊢ φ \to C \in (F^{-1} {lim}_{ℂ} F (C))$
80	75 79	sseldd	$⊢ φ \to C \in ((z \in (Y ∖ \{F (C)\}) ⟼ F^{-1} (z)) {lim}_{ℂ} F (C))$
81	47 37 9	dvlem	$⊢ (φ \land y \in (X ∖ \{C\})) \to \frac{F (y) - F (C)}{y - C} \in ℂ$
82	39 42 54	subne0d	$⊢ (φ \land y \in (X ∖ \{C\})) \to y - C \neq 0$
83	52 43 65 82	divne0d	$⊢ (φ \land y \in (X ∖ \{C\})) \to \frac{F (y) - F (C)}{y - C} \neq 0$
84		eldifsn	$⊢ \frac{F (y) - F (C)}{y - C} \in (ℂ ∖ \{0\}) \leftrightarrow (\frac{F (y) - F (C)}{y - C} \in ℂ \land \frac{F (y) - F (C)}{y - C} \neq 0)$
85	81 83 84	sylanbrc	$⊢ (φ \land y \in (X ∖ \{C\})) \to \frac{F (y) - F (C)}{y - C} \in (ℂ ∖ \{0\})$
86	85	fmpttd	$⊢ φ \to (y \in (X ∖ \{C\}) ⟼ \frac{F (y) - F (C)}{y - C}) : X ∖ \{C\} ⟶ ℂ ∖ \{0\}$
87		difss	$⊢ ℂ ∖ \{0\} \subseteq ℂ$
88	87	a1i	$⊢ φ \to ℂ ∖ \{0\} \subseteq ℂ$
89		eqid	$⊢ J ↾_{𝑡} (ℂ ∖ \{0\}) = J ↾_{𝑡} (ℂ ∖ \{0\})$
90	9 7	eleqtrrd	$⊢ φ \to C \in dom F_{S}^{'}$
91		dvfg	$⊢ S \in \{ℝ, ℂ\} \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
92		ffun	$⊢ F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \to Fun F_{S}^{'}$
93		funfvbrb	$⊢ Fun F_{S}^{'} \to (C \in dom F_{S}^{'} \leftrightarrow C F_{S}^{'} F_{S}^{'} (C))$
94	3 91 92 93	4syl	$⊢ φ \to (C \in dom F_{S}^{'} \leftrightarrow C F_{S}^{'} F_{S}^{'} (C))$
95	90 94	mpbid	$⊢ φ \to C F_{S}^{'} F_{S}^{'} (C)$
96		eqid	$⊢ (y \in (X ∖ \{C\}) ⟼ \frac{F (y) - F (C)}{y - C}) = (y \in (X ∖ \{C\}) ⟼ \frac{F (y) - F (C)}{y - C})$
97	2 1 96 15 47 36	eldv	$⊢ φ \to (C F_{S}^{'} F_{S}^{'} (C) \leftrightarrow (C \in int (K) (X) \land F_{S}^{'} (C) \in ((y \in (X ∖ \{C\}) ⟼ \frac{F (y) - F (C)}{y - C}) {lim}_{ℂ} C)))$
98	95 97	mpbid	$⊢ φ \to (C \in int (K) (X) \land F_{S}^{'} (C) \in ((y \in (X ∖ \{C\}) ⟼ \frac{F (y) - F (C)}{y - C}) {lim}_{ℂ} C))$
99	98	simprd	$⊢ φ \to F_{S}^{'} (C) \in ((y \in (X ∖ \{C\}) ⟼ \frac{F (y) - F (C)}{y - C}) {lim}_{ℂ} C)$
100		resttopon	$⊢ (J \in TopOn (ℂ) \land ℂ ∖ \{0\} \subseteq ℂ) \to J ↾_{𝑡} (ℂ ∖ \{0\}) \in TopOn (ℂ ∖ \{0\})$
101	13 87 100	mp2an	$⊢ J ↾_{𝑡} (ℂ ∖ \{0\}) \in TopOn (ℂ ∖ \{0\})$
102	101	a1i	$⊢ φ \to J ↾_{𝑡} (ℂ ∖ \{0\}) \in TopOn (ℂ ∖ \{0\})$
103	13	a1i	$⊢ φ \to J \in TopOn (ℂ)$
104		1cnd	$⊢ φ \to 1 \in ℂ$
105	102 103 104	cnmptc	$⊢ φ \to (x \in (ℂ ∖ \{0\}) ⟼ 1) \in ((J ↾_{𝑡} (ℂ ∖ \{0\})) Cn J)$
106	102	cnmptid	$⊢ φ \to (x \in (ℂ ∖ \{0\}) ⟼ x) \in ((J ↾_{𝑡} (ℂ ∖ \{0\})) Cn (J ↾_{𝑡} (ℂ ∖ \{0\})))$
107	1 89	divcn	$⊢ \div \in ((J \times_{t} (J ↾_{𝑡} (ℂ ∖ \{0\}))) Cn J)$
108	107	a1i	$⊢ φ \to \div \in ((J \times_{t} (J ↾_{𝑡} (ℂ ∖ \{0\}))) Cn J)$
109	102 105 106 108	cnmpt12f	$⊢ φ \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x}) \in ((J ↾_{𝑡} (ℂ ∖ \{0\})) Cn J)$
110	3 91	syl	$⊢ φ \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
111	7	feq2d	$⊢ φ \to (F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \leftrightarrow F_{S}^{'} : X ⟶ ℂ)$
112	110 111	mpbid	$⊢ φ \to F_{S}^{'} : X ⟶ ℂ$
113	112 9	ffvelrnd	$⊢ φ \to F_{S}^{'} (C) \in ℂ$
114	110	ffnd	$⊢ φ \to F_{S}^{'} Fn dom F_{S}^{'}$
115		fnfvelrn	$⊢ (F_{S}^{'} Fn dom F_{S}^{'} \land C \in dom F_{S}^{'}) \to F_{S}^{'} (C) \in ran F_{S}^{'}$
116	114 90 115	syl2anc	$⊢ φ \to F_{S}^{'} (C) \in ran F_{S}^{'}$
117		nelne2	$⊢ (F_{S}^{'} (C) \in ran F_{S}^{'} \land \neg 0 \in ran F_{S}^{'}) \to F_{S}^{'} (C) \neq 0$
118	116 8 117	syl2anc	$⊢ φ \to F_{S}^{'} (C) \neq 0$
119		eldifsn	$⊢ F_{S}^{'} (C) \in (ℂ ∖ \{0\}) \leftrightarrow (F_{S}^{'} (C) \in ℂ \land F_{S}^{'} (C) \neq 0)$
120	113 118 119	sylanbrc	$⊢ φ \to F_{S}^{'} (C) \in (ℂ ∖ \{0\})$
121	101	toponunii	$⊢ ℂ ∖ \{0\} = ⋃ (J ↾_{𝑡} (ℂ ∖ \{0\}))$
122	121	cncnpi	$⊢ ((x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x}) \in ((J ↾_{𝑡} (ℂ ∖ \{0\})) Cn J) \land F_{S}^{'} (C) \in (ℂ ∖ \{0\})) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x}) \in ((J ↾_{𝑡} (ℂ ∖ \{0\})) CnP J) (F_{S}^{'} (C))$
123	109 120 122	syl2anc	$⊢ φ \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x}) \in ((J ↾_{𝑡} (ℂ ∖ \{0\})) CnP J) (F_{S}^{'} (C))$
124	86 88 1 89 99 123	limccnp	$⊢ φ \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x}) (F_{S}^{'} (C)) \in (((x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x}) \circ (y \in (X ∖ \{C\}) ⟼ \frac{F (y) - F (C)}{y - C})) {lim}_{ℂ} C)$
125		oveq2	$⊢ x = F_{S}^{'} (C) \to \frac{1}{x} = \frac{1}{F_{S}^{'} (C)}$
126		eqid	$⊢ (x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x}) = (x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x})$
127		ovex	$⊢ \frac{1}{F_{S}^{'} (C)} \in V$
128	125 126 127	fvmpt	$⊢ F_{S}^{'} (C) \in (ℂ ∖ \{0\}) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x}) (F_{S}^{'} (C)) = \frac{1}{F_{S}^{'} (C)}$
129	120 128	syl	$⊢ φ \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x}) (F_{S}^{'} (C)) = \frac{1}{F_{S}^{'} (C)}$
130		eqidd	$⊢ φ \to (y \in (X ∖ \{C\}) ⟼ \frac{F (y) - F (C)}{y - C}) = (y \in (X ∖ \{C\}) ⟼ \frac{F (y) - F (C)}{y - C})$
131		eqidd	$⊢ φ \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x}) = (x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x})$
132		oveq2	$⊢ x = \frac{F (y) - F (C)}{y - C} \to \frac{1}{x} = \frac{1}{\frac{F (y) - F (C)}{y - C}}$
133	85 130 131 132	fmptco	$⊢ φ \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x}) \circ (y \in (X ∖ \{C\}) ⟼ \frac{F (y) - F (C)}{y - C}) = (y \in (X ∖ \{C\}) ⟼ \frac{1}{\frac{F (y) - F (C)}{y - C}})$
134	52 43 65 82	recdivd	$⊢ (φ \land y \in (X ∖ \{C\})) \to \frac{1}{\frac{F (y) - F (C)}{y - C}} = \frac{y - C}{F (y) - F (C)}$
135	134	mpteq2dva	$⊢ φ \to (y \in (X ∖ \{C\}) ⟼ \frac{1}{\frac{F (y) - F (C)}{y - C}}) = (y \in (X ∖ \{C\}) ⟼ \frac{y - C}{F (y) - F (C)})$
136	133 135	eqtrd	$⊢ φ \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x}) \circ (y \in (X ∖ \{C\}) ⟼ \frac{F (y) - F (C)}{y - C}) = (y \in (X ∖ \{C\}) ⟼ \frac{y - C}{F (y) - F (C)})$
137	136	oveq1d	$⊢ φ \to ((x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x}) \circ (y \in (X ∖ \{C\}) ⟼ \frac{F (y) - F (C)}{y - C})) {lim}_{ℂ} C = (y \in (X ∖ \{C\}) ⟼ \frac{y - C}{F (y) - F (C)}) {lim}_{ℂ} C$
138	124 129 137	3eltr3d	$⊢ φ \to \frac{1}{F_{S}^{'} (C)} \in ((y \in (X ∖ \{C\}) ⟼ \frac{y - C}{F (y) - F (C)}) {lim}_{ℂ} C)$
139		oveq1	$⊢ y = F^{-1} (z) \to y - C = F^{-1} (z) - C$
140		fveq2	$⊢ y = F^{-1} (z) \to F (y) = F (F^{-1} (z))$
141	140	oveq1d	$⊢ y = F^{-1} (z) \to F (y) - F (C) = F (F^{-1} (z)) - F (C)$
142	139 141	oveq12d	$⊢ y = F^{-1} (z) \to \frac{y - C}{F (y) - F (C)} = \frac{F^{-1} (z) - C}{F (F^{-1} (z)) - F (C)}$
143		eldifsni	$⊢ z \in (Y ∖ \{F (C)\}) \to z \neq F (C)$
144	143	adantl	$⊢ (φ \land z \in (Y ∖ \{F (C)\})) \to z \neq F (C)$
145	144	necomd	$⊢ (φ \land z \in (Y ∖ \{F (C)\})) \to F (C) \neq z$
146		f1ocnvfvb	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land C \in X \land z \in Y) \to (F (C) = z \leftrightarrow F^{-1} (z) = C)$
147	5 9 27 146	syl2an3an	$⊢ (φ \land z \in (Y ∖ \{F (C)\})) \to (F (C) = z \leftrightarrow F^{-1} (z) = C)$
148	147	necon3abid	$⊢ (φ \land z \in (Y ∖ \{F (C)\})) \to (F (C) \neq z \leftrightarrow \neg F^{-1} (z) = C)$
149	145 148	mpbid	$⊢ (φ \land z \in (Y ∖ \{F (C)\})) \to \neg F^{-1} (z) = C$
150	149	pm2.21d	$⊢ (φ \land z \in (Y ∖ \{F (C)\})) \to (F^{-1} (z) = C \to \frac{F^{-1} (z) - C}{F (F^{-1} (z)) - F (C)} = \frac{1}{F_{S}^{'} (C)})$
151	150	impr	$⊢ (φ \land (z \in (Y ∖ \{F (C)\}) \land F^{-1} (z) = C)) \to \frac{F^{-1} (z) - C}{F (F^{-1} (z)) - F (C)} = \frac{1}{F_{S}^{'} (C)}$
152	33 66 80 138 142 151	limcco	$⊢ φ \to \frac{1}{F_{S}^{'} (C)} \in ((z \in (Y ∖ \{F (C)\}) ⟼ \frac{F^{-1} (z) - C}{F (F^{-1} (z)) - F (C)}) {lim}_{ℂ} F (C))$
153	77	eqcomd	$⊢ φ \to C = F^{-1} (F (C))$
154	153	adantr	$⊢ (φ \land z \in (Y ∖ \{F (C)\})) \to C = F^{-1} (F (C))$
155	154	oveq2d	$⊢ (φ \land z \in (Y ∖ \{F (C)\})) \to F^{-1} (z) - C = F^{-1} (z) - F^{-1} (F (C))$
156		f1ocnvfv2	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land z \in Y) \to F (F^{-1} (z)) = z$
157	5 27 156	syl2an	$⊢ (φ \land z \in (Y ∖ \{F (C)\})) \to F (F^{-1} (z)) = z$
158	157	oveq1d	$⊢ (φ \land z \in (Y ∖ \{F (C)\})) \to F (F^{-1} (z)) - F (C) = z - F (C)$
159	155 158	oveq12d	$⊢ (φ \land z \in (Y ∖ \{F (C)\})) \to \frac{F^{-1} (z) - C}{F (F^{-1} (z)) - F (C)} = \frac{F^{-1} (z) - F^{-1} (F (C))}{z - F (C)}$
160	159	mpteq2dva	$⊢ φ \to (z \in (Y ∖ \{F (C)\}) ⟼ \frac{F^{-1} (z) - C}{F (F^{-1} (z)) - F (C)}) = (z \in (Y ∖ \{F (C)\}) ⟼ \frac{F^{-1} (z) - F^{-1} (F (C))}{z - F (C)})$
161	160	oveq1d	$⊢ φ \to (z \in (Y ∖ \{F (C)\}) ⟼ \frac{F^{-1} (z) - C}{F (F^{-1} (z)) - F (C)}) {lim}_{ℂ} F (C) = (z \in (Y ∖ \{F (C)\}) ⟼ \frac{F^{-1} (z) - F^{-1} (F (C))}{z - F (C)}) {lim}_{ℂ} F (C)$
162	152 161	eleqtrd	$⊢ φ \to \frac{1}{F_{S}^{'} (C)} \in ((z \in (Y ∖ \{F (C)\}) ⟼ \frac{F^{-1} (z) - F^{-1} (F (C))}{z - F (C)}) {lim}_{ℂ} F (C))$
163		eqid	$⊢ (z \in (Y ∖ \{F (C)\}) ⟼ \frac{F^{-1} (z) - F^{-1} (F (C))}{z - F (C)}) = (z \in (Y ∖ \{F (C)\}) ⟼ \frac{F^{-1} (z) - F^{-1} (F (C))}{z - F (C)})$
164	26 37	fssd	$⊢ φ \to F^{-1} : Y ⟶ ℂ$
165	2 1 163 15 164 45	eldv	$⊢ φ \to (F (C) {F^{-1}}_{S}^{'} (\frac{1}{F_{S}^{'} (C)}) \leftrightarrow (F (C) \in int (K) (Y) \land \frac{1}{F_{S}^{'} (C)} \in ((z \in (Y ∖ \{F (C)\}) ⟼ \frac{F^{-1} (z) - F^{-1} (F (C))}{z - F (C)}) {lim}_{ℂ} F (C))))$
166	23 162 165	mpbir2and	$⊢ φ \to F (C) {F^{-1}}_{S}^{'} (\frac{1}{F_{S}^{'} (C)})$

Metamath Proof Explorer

Theorem dvcnvlem

Proof