ipasslem7 - Metamath Proof Explorer

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

Theorem ipasslem7 31264

Description: Lemma for ipassi 31269. Show that ((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵)) is continuous on ℝ. (Contributed by NM, 23-Aug-2007.) (Revised by Mario Carneiro, 6-May-2014.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
ip1i.1	⊢ 𝑋 = (BaseSet‘𝑈)
ip1i.2	⊢ 𝐺 = ( +_𝑣 ‘𝑈)
ip1i.4	⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
ip1i.7	⊢ 𝑃 = (·_𝑖OLD‘𝑈)
ip1i.9	⊢ 𝑈 ∈ CPreHil_OLD
ipasslem7.a	⊢ 𝐴 ∈ 𝑋
ipasslem7.b	⊢ 𝐵 ∈ 𝑋
ipasslem7.f	⊢ 𝐹 = (𝑤 ∈ ℝ ↦ (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵))))
ipasslem7.j	⊢ 𝐽 = (topGen‘ran (,))
ipasslem7.k	⊢ 𝐾 = (TopOpen‘ℂ_fld)

**Assertion**
Ref	Expression
ipasslem7	⊢ 𝐹 ∈ (𝐽 Cn 𝐾)

Distinct variable groups: 𝑤,𝐵 𝑤,𝐾 𝑤,𝑃 𝑤,𝑆 𝑤,𝑈 𝑤,𝑋 𝑤,𝐴 Allowed substitution hints: 𝐹(𝑤) 𝐺(𝑤) 𝐽(𝑤)

**Proof of Theorem ipasslem7**
Step	Hyp	Ref	Expression
1		ipasslem7.f	. 2 ⊢ 𝐹 = (𝑤 ∈ ℝ ↦ (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵))))
2		ipasslem7.j	. . . . 5 ⊢ 𝐽 = (topGen‘ran (,))
3		ipasslem7.k	. . . . . 6 ⊢ 𝐾 = (TopOpen‘ℂ_fld)
4	3	tgioo2 25016	. . . . 5 ⊢ (topGen‘ran (,)) = (𝐾 ↾_t ℝ)
5	2, 4	eqtri 2788	. . . 4 ⊢ 𝐽 = (𝐾 ↾_t ℝ)
6	3	cnfldtopon 24995	. . . . 5 ⊢ 𝐾 ∈ (TopOn‘ℂ)
7	6	a1i 11	. . . 4 ⊢ (⊤ → 𝐾 ∈ (TopOn‘ℂ))
8		ax-resscn 11177	. . . . 5 ⊢ ℝ ⊆ ℂ
9	8	a1i 11	. . . 4 ⊢ (⊤ → ℝ ⊆ ℂ)
10	7	cnmptid 23874	. . . . . . 7 ⊢ (⊤ → (𝑤 ∈ ℂ ↦ 𝑤) ∈ (𝐾 Cn 𝐾))
11		ip1i.9	. . . . . . . . . . 11 ⊢ 𝑈 ∈ CPreHil_OLD
12	11	phnvi 31244	. . . . . . . . . 10 ⊢ 𝑈 ∈ NrmCVec
13		ip1i.1	. . . . . . . . . . 11 ⊢ 𝑋 = (BaseSet‘𝑈)
14		eqid 2765	. . . . . . . . . . 11 ⊢ (IndMet‘𝑈) = (IndMet‘𝑈)
15	13, 14	imsxmet 31120	. . . . . . . . . 10 ⊢ (𝑈 ∈ NrmCVec → (IndMet‘𝑈) ∈ (∞Met‘𝑋))
16	12, 15	ax-mp 5	. . . . . . . . 9 ⊢ (IndMet‘𝑈) ∈ (∞Met‘𝑋)
17		eqid 2765	. . . . . . . . . 10 ⊢ (MetOpen‘(IndMet‘𝑈)) = (MetOpen‘(IndMet‘𝑈))
18	17	mopntopon 24652	. . . . . . . . 9 ⊢ ((IndMet‘𝑈) ∈ (∞Met‘𝑋) → (MetOpen‘(IndMet‘𝑈)) ∈ (TopOn‘𝑋))
19	16, 18	mp1i 14	. . . . . . . 8 ⊢ (⊤ → (MetOpen‘(IndMet‘𝑈)) ∈ (TopOn‘𝑋))
20		ipasslem7.a	. . . . . . . . 9 ⊢ 𝐴 ∈ 𝑋
21	20	a1i 11	. . . . . . . 8 ⊢ (⊤ → 𝐴 ∈ 𝑋)
22	7, 19, 21	cnmptc 23875	. . . . . . 7 ⊢ (⊤ → (𝑤 ∈ ℂ ↦ 𝐴) ∈ (𝐾 Cn (MetOpen‘(IndMet‘𝑈))))
23		ip1i.4	. . . . . . . . 9 ⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
24	14, 17, 23, 3	smcn 31126	. . . . . . . 8 ⊢ (𝑈 ∈ NrmCVec → 𝑆 ∈ ((𝐾 ×_t (MetOpen‘(IndMet‘𝑈))) Cn (MetOpen‘(IndMet‘𝑈))))
25	12, 24	mp1i 14	. . . . . . 7 ⊢ (⊤ → 𝑆 ∈ ((𝐾 ×_t (MetOpen‘(IndMet‘𝑈))) Cn (MetOpen‘(IndMet‘𝑈))))
26	7, 10, 22, 25	cnmpt12f 23879	. . . . . 6 ⊢ (⊤ → (𝑤 ∈ ℂ ↦ (𝑤𝑆𝐴)) ∈ (𝐾 Cn (MetOpen‘(IndMet‘𝑈))))
27		ipasslem7.b	. . . . . . . 8 ⊢ 𝐵 ∈ 𝑋
28	27	a1i 11	. . . . . . 7 ⊢ (⊤ → 𝐵 ∈ 𝑋)
29	7, 19, 28	cnmptc 23875	. . . . . 6 ⊢ (⊤ → (𝑤 ∈ ℂ ↦ 𝐵) ∈ (𝐾 Cn (MetOpen‘(IndMet‘𝑈))))
30		ip1i.7	. . . . . . . 8 ⊢ 𝑃 = (·_𝑖OLD‘𝑈)
31	30, 14, 17, 3	dipcn 31148	. . . . . . 7 ⊢ (𝑈 ∈ NrmCVec → 𝑃 ∈ (((MetOpen‘(IndMet‘𝑈)) ×_t (MetOpen‘(IndMet‘𝑈))) Cn 𝐾))
32	12, 31	mp1i 14	. . . . . 6 ⊢ (⊤ → 𝑃 ∈ (((MetOpen‘(IndMet‘𝑈)) ×_t (MetOpen‘(IndMet‘𝑈))) Cn 𝐾))
33	7, 26, 29, 32	cnmpt12f 23879	. . . . 5 ⊢ (⊤ → (𝑤 ∈ ℂ ↦ ((𝑤𝑆𝐴)𝑃𝐵)) ∈ (𝐾 Cn 𝐾))
34	13, 30	dipcl 31140	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) ∈ ℂ)
35	12, 20, 27, 34	mp3an 1490	. . . . . . . 8 ⊢ (𝐴𝑃𝐵) ∈ ℂ
36	35	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝐴𝑃𝐵) ∈ ℂ)
37	7, 7, 36	cnmptc 23875	. . . . . 6 ⊢ (⊤ → (𝑤 ∈ ℂ ↦ (𝐴𝑃𝐵)) ∈ (𝐾 Cn 𝐾))
38	3	mulcn 25081	. . . . . . 7 ⊢ · ∈ ((𝐾 ×_t 𝐾) Cn 𝐾)
39	38	a1i 11	. . . . . 6 ⊢ (⊤ → · ∈ ((𝐾 ×_t 𝐾) Cn 𝐾))
40	7, 10, 37, 39	cnmpt12f 23879	. . . . 5 ⊢ (⊤ → (𝑤 ∈ ℂ ↦ (𝑤 · (𝐴𝑃𝐵))) ∈ (𝐾 Cn 𝐾))
41	3	subcn 25080	. . . . . 6 ⊢ − ∈ ((𝐾 ×_t 𝐾) Cn 𝐾)
42	41	a1i 11	. . . . 5 ⊢ (⊤ → − ∈ ((𝐾 ×_t 𝐾) Cn 𝐾))
43	7, 33, 40, 42	cnmpt12f 23879	. . . 4 ⊢ (⊤ → (𝑤 ∈ ℂ ↦ (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵)))) ∈ (𝐾 Cn 𝐾))
44	5, 7, 9, 43	cnmpt1res 23889	. . 3 ⊢ (⊤ → (𝑤 ∈ ℝ ↦ (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵)))) ∈ (𝐽 Cn 𝐾))
45	44	mptru 1577	. 2 ⊢ (𝑤 ∈ ℝ ↦ (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵)))) ∈ (𝐽 Cn 𝐾)
46	1, 45	eqeltri 2861	1 ⊢ 𝐹 ∈ (𝐽 Cn 𝐾)

Colors of variables: wff setvar class

This proof depends on syntax axioms: = wceq 1570 ⊤wtru 1571 ∈ wcel 2146 ⊆ wss 3906 ↦ cmpt 5194 ran crn 5664 ‘cfv 6541 (class class class)co 7420 ℂcc 11118 ℝcr 11119 · cmul 11125 − cmin 11461 (,)cioo 13393 ↾_t crest 17500 TopOpenctopn 17501 topGenctg 17517 ∞Metcxmet 21562 MetOpencmopn 21567 ℂ_fldccnfld 21577 TopOnctopon 23122 Cn ccn 23436 ×_t ctx 23773 NrmCVeccnv 31012 +_𝑣 cpv 31013 BaseSetcba 31014 ·_𝑠OLD cns 31015 IndMetcims 31019 ·_𝑖OLDcdip 31128 CPreHil_OLDccphlo 31240

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7743 ax-inf2 9618 ax-cnex 11176 ax-resscn 11177 ax-1cn 11178 ax-icn 11179 ax-addcl 11180 ax-addrcl 11181 ax-mulcl 11182 ax-mulrcl 11183 ax-mulcom 11184 ax-addass 11185 ax-mulass 11186 ax-distr 11187 ax-i2m1 11188 ax-1ne0 11189 ax-1rid 11190 ax-rnegex 11191 ax-rrecex 11192 ax-cnre 11193 ax-pre-lttri 11194 ax-pre-lttrn 11195 ax-pre-ltadd 11196 ax-pre-mulgt0 11197 ax-pre-sup 11198 ax-addf 11199 ax-mulf 11200

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7685 df-om 7870 df-1st 7993 df-2nd 7994 df-supp 8164 df-frecs 8285 df-wrecs 8316 df-recs 8365 df-rdg 8404 df-1o 8460 df-2o 8461 df-er 8701 df-map 8833 df-ixp 8903 df-en 8951 df-dom 8952 df-sdom 8953 df-fin 8954 df-fsupp 9330 df-fi 9379 df-sup 9410 df-inf 9411 df-oi 9480 df-card 9942 df-pnf 11265 df-mnf 11266 df-xr 11267 df-ltxr 11268 df-le 11269 df-sub 11463 df-neg 11464 df-div 11892 df-nn 12254 df-2 12323 df-3 12324 df-4 12325 df-5 12326 df-6 12327 df-7 12328 df-8 12329 df-9 12330 df-n0 12525 df-z 12612 df-dec 12733 df-uz 12884 df-q 12994 df-rp 13038 df-xneg 13158 df-xadd 13159 df-xmul 13160 df-ioo 13397 df-icc 13400 df-fz 13557 df-fzo 13705 df-seq 14061 df-exp 14121 df-hash 14390 df-cj 15179 df-re 15180 df-im 15181 df-sqrt 15315 df-abs 15316 df-clim 15568 df-sum 15767 df-struct 17234 df-sets 17251 df-slot 17269 df-ndx 17281 df-base 17297 df-ress 17318 df-plusg 17350 df-mulr 17351 df-starv 17352 df-sca 17353 df-vsca 17354 df-ip 17355 df-tset 17356 df-ple 17357 df-ds 17359 df-unif 17360 df-hom 17361 df-cco 17362 df-rest 17502 df-topn 17503 df-0g 17521 df-gsum 17522 df-topgen 17523 df-pt 17524 df-prds 17527 df-xrs 17583 df-qtop 17588 df-imas 17589 df-xps 17591 df-mre 17665 df-mrc 17666 df-acs 17668 df-mgm 18725 df-sgrp 18814 df-mnd 18830 df-submnd 18884 df-mulg 19183 df-cntz 19436 df-cmn 19901 df-psmet 21569 df-xmet 21570 df-met 21571 df-bl 21572 df-mopn 21573 df-cnfld 21578 df-top 23106 df-topon 23123 df-topsp 23145 df-bases 23158 df-cn 23439 df-cnp 23440 df-tx 23775 df-hmeo 23968 df-xms 24533 df-ms 24534 df-tms 24535 df-grpo 30921 df-gid 30922 df-ginv 30923 df-gdiv 30924 df-ablo 30973 df-vc 30987 df-nv 31020 df-va 31023 df-ba 31024 df-sm 31025 df-0v 31026 df-vs 31027 df-nmcv 31028 df-ims 31029 df-dip 31129 df-ph 31241

This theorem is used by: ipasslem8 31265

W3C validator