dvcnv

Description: A weak version of dvcnvre , valid for both real and complex domains but under the hypothesis that the inverse function is already known to be continuous, and the image set is known to be open. A more advanced proof can show that these conditions are unnecessary. (Contributed by Mario Carneiro, 25-Feb-2015) (Revised by Mario Carneiro, 8-Sep-2015)

	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}^{'}$
Assertion	dvcnv	$⊢ φ \to S D F^{-1} = (x \in Y ⟼ \frac{1}{F_{S}^{'} (F^{-1} (x))})$

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		dvfg	$⊢ S \in \{ℝ, ℂ\} \to {F^{-1}}_{S}^{'} : dom {F^{-1}}_{S}^{'} ⟶ ℂ$
10	3 9	syl	$⊢ φ \to {F^{-1}}_{S}^{'} : dom {F^{-1}}_{S}^{'} ⟶ ℂ$
11		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
12	3 11	syl	$⊢ φ \to S \subseteq ℂ$
13		f1ocnv	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F^{-1} : Y \underset{1-1 onto}{⟶} X$
14		f1of	$⊢ F^{-1} : Y \underset{1-1 onto}{⟶} X \to F^{-1} : Y ⟶ X$
15	5 13 14	3syl	$⊢ φ \to F^{-1} : Y ⟶ X$
16		dvbsss	$⊢ dom F_{S}^{'} \subseteq S$
17	7 16	eqsstrrdi	$⊢ φ \to X \subseteq S$
18	17 12	sstrd	$⊢ φ \to X \subseteq ℂ$
19	15 18	fssd	$⊢ φ \to F^{-1} : Y ⟶ ℂ$
20	1	cnfldtopon	$⊢ J \in TopOn (ℂ)$
21		resttopon	$⊢ (J \in TopOn (ℂ) \land S \subseteq ℂ) \to J ↾_{𝑡} S \in TopOn (S)$
22	20 12 21	sylancr	$⊢ φ \to J ↾_{𝑡} S \in TopOn (S)$
23	2 22	eqeltrid	$⊢ φ \to K \in TopOn (S)$
24		toponss	$⊢ (K \in TopOn (S) \land Y \in K) \to Y \subseteq S$
25	23 4 24	syl2anc	$⊢ φ \to Y \subseteq S$
26	12 19 25	dvbss	$⊢ φ \to dom {F^{-1}}_{S}^{'} \subseteq Y$
27		f1ocnvfv2	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land x \in Y) \to F (F^{-1} (x)) = x$
28	5 27	sylan	$⊢ (φ \land x \in Y) \to F (F^{-1} (x)) = x$
29	3	adantr	$⊢ (φ \land x \in Y) \to S \in \{ℝ, ℂ\}$
30	4	adantr	$⊢ (φ \land x \in Y) \to Y \in K$
31	5	adantr	$⊢ (φ \land x \in Y) \to F : X \underset{1-1 onto}{⟶} Y$
32	6	adantr	$⊢ (φ \land x \in Y) \to F^{-1} : Y \underset{cn}{⟶} X$
33	7	adantr	$⊢ (φ \land x \in Y) \to dom F_{S}^{'} = X$
34	8	adantr	$⊢ (φ \land x \in Y) \to \neg 0 \in ran F_{S}^{'}$
35	15	ffvelrnda	$⊢ (φ \land x \in Y) \to F^{-1} (x) \in X$
36	1 2 29 30 31 32 33 34 35	dvcnvlem	$⊢ (φ \land x \in Y) \to F (F^{-1} (x)) {F^{-1}}_{S}^{'} (\frac{1}{F_{S}^{'} (F^{-1} (x))})$
37	28 36	eqbrtrrd	$⊢ (φ \land x \in Y) \to x {F^{-1}}_{S}^{'} (\frac{1}{F_{S}^{'} (F^{-1} (x))})$
38		reldv	$⊢ Rel {F^{-1}}_{S}^{'}$
39	38	releldmi	$⊢ x {F^{-1}}_{S}^{'} (\frac{1}{F_{S}^{'} (F^{-1} (x))}) \to x \in dom {F^{-1}}_{S}^{'}$
40	37 39	syl	$⊢ (φ \land x \in Y) \to x \in dom {F^{-1}}_{S}^{'}$
41	26 40	eqelssd	$⊢ φ \to dom {F^{-1}}_{S}^{'} = Y$
42	41	feq2d	$⊢ φ \to ({F^{-1}}_{S}^{'} : dom {F^{-1}}_{S}^{'} ⟶ ℂ \leftrightarrow {F^{-1}}_{S}^{'} : Y ⟶ ℂ)$
43	10 42	mpbid	$⊢ φ \to {F^{-1}}_{S}^{'} : Y ⟶ ℂ$
44	43	feqmptd	$⊢ φ \to S D F^{-1} = (x \in Y ⟼ {F^{-1}}_{S}^{'} (x))$
45	10	adantr	$⊢ (φ \land x \in Y) \to {F^{-1}}_{S}^{'} : dom {F^{-1}}_{S}^{'} ⟶ ℂ$
46	45	ffund	$⊢ (φ \land x \in Y) \to Fun {F^{-1}}_{S}^{'}$
47		funbrfv	$⊢ Fun {F^{-1}}_{S}^{'} \to (x {F^{-1}}_{S}^{'} (\frac{1}{F_{S}^{'} (F^{-1} (x))}) \to {F^{-1}}_{S}^{'} (x) = \frac{1}{F_{S}^{'} (F^{-1} (x))})$
48	46 37 47	sylc	$⊢ (φ \land x \in Y) \to {F^{-1}}_{S}^{'} (x) = \frac{1}{F_{S}^{'} (F^{-1} (x))}$
49	48	mpteq2dva	$⊢ φ \to (x \in Y ⟼ {F^{-1}}_{S}^{'} (x)) = (x \in Y ⟼ \frac{1}{F_{S}^{'} (F^{-1} (x))})$
50	44 49	eqtrd	$⊢ φ \to S D F^{-1} = (x \in Y ⟼ \frac{1}{F_{S}^{'} (F^{-1} (x))})$

Metamath Proof Explorer

Theorem dvcnv

Proof