Metamath Proof Explorer

Theorem 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 𝐹 ) ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) ) )