dvcnv - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dvcnv		Structured version Visualization version GIF version

Theorem dvcnv 26306

Description: A weak version of dvcnvre 26348, 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.)

**Hypotheses**
Ref	Expression
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**
Ref	Expression
dvcnv	⊢ (𝜑 → (𝑆 D ^◡𝐹) = (𝑥 ∈ 𝑌 ↦ (1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥)))))

Distinct variable groups: 𝑥,𝐹 𝑥,𝐽 𝜑,𝑥 𝑥,𝑆 𝑥,𝑌 Allowed substitution hints: 𝐾(𝑥) 𝑋(𝑥)

**Proof of Theorem dvcnv**
Step	Hyp	Ref	Expression
1		dvcnv.s	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
2		dvfg 26235	. . . . 5 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D ^◡𝐹):dom (𝑆 D ^◡𝐹)⟶ℂ)
3	1, 2	syl 18	. . . 4 ⊢ (𝜑 → (𝑆 D ^◡𝐹):dom (𝑆 D ^◡𝐹)⟶ℂ)
4		recnprss 26233	. . . . . . . 8 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
5	1, 4	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
6		dvcnv.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌)
7		f1ocnv 6842	. . . . . . . . 9 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → ^◡𝐹:𝑌–1-1-onto→𝑋)
8		f1of 6829	. . . . . . . . 9 ⊢ (^◡𝐹:𝑌–1-1-onto→𝑋 → ^◡𝐹:𝑌⟶𝑋)
9	6, 7, 8	3syl 19	. . . . . . . 8 ⊢ (𝜑 → ^◡𝐹:𝑌⟶𝑋)
10		dvcnv.d	. . . . . . . . . 10 ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)
11		dvbsss 26231	. . . . . . . . . 10 ⊢ dom (𝑆 D 𝐹) ⊆ 𝑆
12	10, 11	eqsstrrdi 3954	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
13	12, 5	sstrd 3919	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
14	9, 13	fssd 6732	. . . . . . 7 ⊢ (𝜑 → ^◡𝐹:𝑌⟶ℂ)
15		dvcnv.k	. . . . . . . . 9 ⊢ 𝐾 = (𝐽 ↾_t 𝑆)
16		dvcnv.j	. . . . . . . . . . 11 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
17	16	cnfldtopon 25110	. . . . . . . . . 10 ⊢ 𝐽 ∈ (TopOn‘ℂ)
18		resttopon 23488	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
19	17, 5, 18	sylancr 599	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
20	15, 19	eqeltrid 2864	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑆))
21		dvcnv.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝐾)
22		toponss 23254	. . . . . . . 8 ⊢ ((𝐾 ∈ (TopOn‘𝑆) ∧ 𝑌 ∈ 𝐾) → 𝑌 ⊆ 𝑆)
23	20, 21, 22	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ 𝑆)
24	5, 14, 23	dvbss 26230	. . . . . 6 ⊢ (𝜑 → dom (𝑆 D ^◡𝐹) ⊆ 𝑌)
25		f1ocnvfv2 7289	. . . . . . . . 9 ⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
26	6, 25	sylan 592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
27	1	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑆 ∈ {ℝ, ℂ})
28	21	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑌 ∈ 𝐾)
29	6	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝐹:𝑋–1-1-onto→𝑌)
30		dvcnv.i	. . . . . . . . . 10 ⊢ (𝜑 → ^◡𝐹 ∈ (𝑌–cn→𝑋))
31	30	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ^◡𝐹 ∈ (𝑌–cn→𝑋))
32	10	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → dom (𝑆 D 𝐹) = 𝑋)
33		dvcnv.z	. . . . . . . . . 10 ⊢ (𝜑 → ¬ 0 ∈ ran (𝑆 D 𝐹))
34	33	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ¬ 0 ∈ ran (𝑆 D 𝐹))
35	9	ffvelcdmda 7089	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (^◡𝐹‘𝑥) ∈ 𝑋)
36	16, 15, 27, 28, 29, 31, 32, 34, 35	dvcnvlem 26305	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥))(𝑆 D ^◡𝐹)(1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥))))
37	26, 36	eqbrtrrd 5128	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥(𝑆 D ^◡𝐹)(1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥))))
38		reldv 26199	. . . . . . . 8 ⊢ Rel (𝑆 D ^◡𝐹)
39	38	releldmi 5931	. . . . . . 7 ⊢ (𝑥(𝑆 D ^◡𝐹)(1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥))) → 𝑥 ∈ dom (𝑆 D ^◡𝐹))
40	37, 39	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ dom (𝑆 D ^◡𝐹))
41	24, 40	eqelssd 3930	. . . . 5 ⊢ (𝜑 → dom (𝑆 D ^◡𝐹) = 𝑌)
42	41	feq2d 6698	. . . 4 ⊢ (𝜑 → ((𝑆 D ^◡𝐹):dom (𝑆 D ^◡𝐹)⟶ℂ ↔ (𝑆 D ^◡𝐹):𝑌⟶ℂ))
43	3, 42	mpbid 235	. . 3 ⊢ (𝜑 → (𝑆 D ^◡𝐹):𝑌⟶ℂ)
44	43	feqmptd 6958	. 2 ⊢ (𝜑 → (𝑆 D ^◡𝐹) = (𝑥 ∈ 𝑌 ↦ ((𝑆 D ^◡𝐹)‘𝑥)))
45	3	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝑆 D ^◡𝐹):dom (𝑆 D ^◡𝐹)⟶ℂ)
46	45	ffund 6719	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → Fun (𝑆 D ^◡𝐹))
47		funbrfv 6938	. . . 4 ⊢ (Fun (𝑆 D ^◡𝐹) → (𝑥(𝑆 D ^◡𝐹)(1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥))) → ((𝑆 D ^◡𝐹)‘𝑥) = (1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥)))))
48	46, 37, 47	sylc 66	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝑆 D ^◡𝐹)‘𝑥) = (1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥))))
49	48	mpteq2dva 5197	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝑌 ↦ ((𝑆 D ^◡𝐹)‘𝑥)) = (𝑥 ∈ 𝑌 ↦ (1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥)))))
50	44, 49	eqtrd 2795	1 ⊢ (𝜑 → (𝑆 D ^◡𝐹) = (𝑥 ∈ 𝑌 ↦ (1 / ((𝑆 D 𝐹)‘(^◡𝐹‘𝑥)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ⊆ wss 3896 {cpr 4586 class class class wbr 5102 ↦ cmpt 5185 ^◡ccnv 5650 dom cdm 5651 ran crn 5652 Fun wfun 6537 ⟶wf 6539 –1-1-onto→wf1o 6542 ‘cfv 6543 (class class class)co 7424 ℂcc 11205 ℝcr 11206 0cc0 11207 1c1 11208 / cdiv 11980 ↾_t crest 17600 TopOpenctopn 17601 ℂ_fldccnfld 21687 TopOnctopon 23237 –cn→ccncf 25206 D cdv 26192

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5327 ax-pr 5391 ax-un 7755 ax-cnex 11263 ax-resscn 11264 ax-1cn 11265 ax-icn 11266 ax-addcl 11267 ax-addrcl 11268 ax-mulcl 11269 ax-mulrcl 11270 ax-mulcom 11271 ax-addass 11272 ax-mulass 11273 ax-distr 11274 ax-i2m1 11275 ax-1ne0 11276 ax-1rid 11277 ax-rnegex 11278 ax-rrecex 11279 ax-cnre 11280 ax-pre-lttri 11281 ax-pre-lttrn 11282 ax-pre-ltadd 11283 ax-pre-mulgt0 11284 ax-pre-sup 11285

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7381 df-ov 7427 df-oprab 7428 df-mpo 7429 df-of 7697 df-om 7882 df-1st 8005 df-2nd 8006 df-supp 8185 df-frecs 8307 df-wrecs 8338 df-recs 8387 df-rdg 8426 df-1o 8484 df-2o 8485 df-er 8725 df-map 8857 df-pm 8858 df-ixp 8934 df-en 8982 df-dom 8983 df-sdom 8984 df-fin 8985 df-fsupp 9362 df-fi 9410 df-sup 9441 df-inf 9442 df-oi 9511 df-card 10027 df-pnf 11352 df-mnf 11353 df-xr 11354 df-ltxr 11355 df-le 11356 df-sub 11550 df-neg 11551 df-div 11981 df-nn 12343 df-2 12412 df-3 12413 df-4 12414 df-5 12415 df-6 12416 df-7 12417 df-8 12418 df-9 12419 df-n0 12614 df-z 12701 df-dec 12822 df-uz 12973 df-q 13083 df-rp 13128 df-xneg 13248 df-xadd 13249 df-xmul 13250 df-icc 13490 df-fz 13647 df-fzo 13796 df-seq 14152 df-exp 14212 df-hash 14482 df-cj 15275 df-re 15276 df-im 15277 df-sqrt 15411 df-abs 15412 df-struct 17334 df-sets 17351 df-slot 17369 df-ndx 17381 df-base 17397 df-ress 17418 df-plusg 17450 df-mulr 17451 df-starv 17452 df-sca 17453 df-vsca 17454 df-ip 17455 df-tset 17456 df-ple 17457 df-ds 17459 df-unif 17460 df-hom 17461 df-cco 17462 df-rest 17602 df-topn 17603 df-0g 17621 df-gsum 17622 df-topgen 17623 df-pt 17624 df-prds 17627 df-xrs 17683 df-qtop 17688 df-imas 17689 df-xps 17691 df-mre 17765 df-mrc 17766 df-acs 17768 df-mgm 18825 df-sgrp 18917 df-mnd 18933 df-submnd 18988 df-mulg 19287 df-cntz 19540 df-cmn 20005 df-psmet 21679 df-xmet 21680 df-met 21681 df-bl 21682 df-mopn 21683 df-fbas 21684 df-fg 21685 df-cnfld 21688 df-top 23221 df-topon 23238 df-topsp 23260 df-bases 23273 df-cld 23346 df-ntr 23347 df-cls 23348 df-nei 23425 df-lp 23463 df-perf 23464 df-cn 23554 df-cnp 23555 df-haus 23642 df-tx 23890 df-hmeo 24083 df-fil 24174 df-fm 24266 df-flim 24267 df-flf 24268 df-xms 24648 df-ms 24649 df-tms 24650 df-cncf 25208 df-limc 26195 df-dv 26196

This theorem is used by: dvcnvre 26348 dvlog 26988

W3C validator