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	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
	dvcnv.k	⊢ 𝐾 = ( 𝐽 ↾_t 𝑆 )
	dvcnv.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	dvcnv.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
	dvcnv.f	⊢ ( 𝜑 → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
	dvcnv.i	⊢ ( 𝜑 → ^◡ 𝐹 ∈ ( 𝑌 –cn→ 𝑋 ) )
	dvcnv.d	⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
	dvcnv.z	⊢ ( 𝜑 → ¬ 0 ∈ ran ( 𝑆 D 𝐹 ) )
Assertion	dvcnv	⊢ ( 𝜑 → ( 𝑆 D ^◡ 𝐹 ) = ( 𝑥 ∈ 𝑌 ↦ ( 1 / ( ( 𝑆 D 𝐹 ) ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvcnv.j	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
2		dvcnv.k	⊢ 𝐾 = ( 𝐽 ↾_t 𝑆 )
3		dvcnv.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
4		dvcnv.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
5		dvcnv.f	⊢ ( 𝜑 → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
6		dvcnv.i	⊢ ( 𝜑 → ^◡ 𝐹 ∈ ( 𝑌 –cn→ 𝑋 ) )
7		dvcnv.d	⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
8		dvcnv.z	⊢ ( 𝜑 → ¬ 0 ∈ ran ( 𝑆 D 𝐹 ) )
9		dvfg	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ^◡ 𝐹 ) : dom ( 𝑆 D ^◡ 𝐹 ) ⟶ ℂ )
10	3 9	syl	⊢ ( 𝜑 → ( 𝑆 D ^◡ 𝐹 ) : dom ( 𝑆 D ^◡ 𝐹 ) ⟶ ℂ )
11		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
12	3 11	syl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
13		f1ocnv	⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ^◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 )
14		f1of	⊢ ( ^◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ^◡ 𝐹 : 𝑌 ⟶ 𝑋 )
15	5 13 14	3syl	⊢ ( 𝜑 → ^◡ 𝐹 : 𝑌 ⟶ 𝑋 )
16		dvbsss	⊢ dom ( 𝑆 D 𝐹 ) ⊆ 𝑆
17	7 16	eqsstrrdi	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
18	17 12	sstrd	⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
19	15 18	fssd	⊢ ( 𝜑 → ^◡ 𝐹 : 𝑌 ⟶ ℂ )
20	1	cnfldtopon	⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
21		resttopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( 𝐽 ↾_t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
22	20 12 21	sylancr	⊢ ( 𝜑 → ( 𝐽 ↾_t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
23	2 22	eqeltrid	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑆 ) )
24		toponss	⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑆 ) ∧ 𝑌 ∈ 𝐾 ) → 𝑌 ⊆ 𝑆 )
25	23 4 24	syl2anc	⊢ ( 𝜑 → 𝑌 ⊆ 𝑆 )
26	12 19 25	dvbss	⊢ ( 𝜑 → dom ( 𝑆 D ^◡ 𝐹 ) ⊆ 𝑌 )
27		f1ocnvfv2	⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
28	5 27	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
29	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑆 ∈ { ℝ , ℂ } )
30	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑌 ∈ 𝐾 )
31	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
32	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ^◡ 𝐹 ∈ ( 𝑌 –cn→ 𝑋 ) )
33	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → dom ( 𝑆 D 𝐹 ) = 𝑋 )
34	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ¬ 0 ∈ ran ( 𝑆 D 𝐹 ) )
35	15	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ^◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 )
36	1 2 29 30 31 32 33 34 35	dvcnvlem	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 𝑆 D ^◡ 𝐹 ) ( 1 / ( ( 𝑆 D 𝐹 ) ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ) )
37	28 36	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ( 𝑆 D ^◡ 𝐹 ) ( 1 / ( ( 𝑆 D 𝐹 ) ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ) )
38		reldv	⊢ Rel ( 𝑆 D ^◡ 𝐹 )
39	38	releldmi	⊢ ( 𝑥 ( 𝑆 D ^◡ 𝐹 ) ( 1 / ( ( 𝑆 D 𝐹 ) ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ) → 𝑥 ∈ dom ( 𝑆 D ^◡ 𝐹 ) )
40	37 39	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ dom ( 𝑆 D ^◡ 𝐹 ) )
41	26 40	eqelssd	⊢ ( 𝜑 → dom ( 𝑆 D ^◡ 𝐹 ) = 𝑌 )
42	41	feq2d	⊢ ( 𝜑 → ( ( 𝑆 D ^◡ 𝐹 ) : dom ( 𝑆 D ^◡ 𝐹 ) ⟶ ℂ ↔ ( 𝑆 D ^◡ 𝐹 ) : 𝑌 ⟶ ℂ ) )
43	10 42	mpbid	⊢ ( 𝜑 → ( 𝑆 D ^◡ 𝐹 ) : 𝑌 ⟶ ℂ )
44	43	feqmptd	⊢ ( 𝜑 → ( 𝑆 D ^◡ 𝐹 ) = ( 𝑥 ∈ 𝑌 ↦ ( ( 𝑆 D ^◡ 𝐹 ) ‘ 𝑥 ) ) )
45	10	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑆 D ^◡ 𝐹 ) : dom ( 𝑆 D ^◡ 𝐹 ) ⟶ ℂ )
46	45	ffund	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → Fun ( 𝑆 D ^◡ 𝐹 ) )
47		funbrfv	⊢ ( Fun ( 𝑆 D ^◡ 𝐹 ) → ( 𝑥 ( 𝑆 D ^◡ 𝐹 ) ( 1 / ( ( 𝑆 D 𝐹 ) ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ) → ( ( 𝑆 D ^◡ 𝐹 ) ‘ 𝑥 ) = ( 1 / ( ( 𝑆 D 𝐹 ) ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ) ) )
48	46 37 47	sylc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑆 D ^◡ 𝐹 ) ‘ 𝑥 ) = ( 1 / ( ( 𝑆 D 𝐹 ) ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ) )
49	48	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑌 ↦ ( ( 𝑆 D ^◡ 𝐹 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑌 ↦ ( 1 / ( ( 𝑆 D 𝐹 ) ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ) ) )
50	44 49	eqtrd	⊢ ( 𝜑 → ( 𝑆 D ^◡ 𝐹 ) = ( 𝑥 ∈ 𝑌 ↦ ( 1 / ( ( 𝑆 D 𝐹 ) ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ) ) )

Metamath Proof Explorer

Theorem dvcnv

Proof