minveclem4b - Metamath Proof Explorer

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

Theorem minveclem4b 25420

Description: Lemma for minvec 25425. The convergent point of the Cauchy sequence 𝐹 is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)

**Hypotheses**
Ref	Expression
minvec.x	⊢ 𝑋 = (Base‘𝑈)
minvec.m	⊢ − = (-_g‘𝑈)
minvec.n	⊢ 𝑁 = (norm‘𝑈)
minvec.u	⊢ (𝜑 → 𝑈 ∈ ℂPreHil)
minvec.y	⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))
minvec.w	⊢ (𝜑 → (𝑈 ↾_s 𝑌) ∈ CMetSp)
minvec.a	⊢ (𝜑 → 𝐴 ∈ 𝑋)
minvec.j	⊢ 𝐽 = (TopOpen‘𝑈)
minvec.r	⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))
minvec.s	⊢ 𝑆 = inf(𝑅, ℝ, < )
minvec.d	⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))
minvec.f	⊢ 𝐹 = ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})
minvec.p	⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))

**Assertion**
Ref	Expression
minveclem4b	⊢ (𝜑 → 𝑃 ∈ 𝑋)

Distinct variable groups: 𝑦, − 𝑦,𝑟,𝐴 𝐽,𝑟,𝑦 𝑦,𝑃 𝑦,𝐹 𝑦,𝑁 𝜑,𝑟,𝑦 𝑦,𝑅 𝑦,𝑈 𝑋,𝑟,𝑦 𝑌,𝑟,𝑦 𝐷,𝑟,𝑦 𝑆,𝑟,𝑦 Allowed substitution hints: 𝑃(𝑟) 𝑅(𝑟) 𝑈(𝑟) 𝐹(𝑟) − (𝑟) 𝑁(𝑟)

**Proof of Theorem minveclem4b**
Step	Hyp	Ref	Expression
1		minvec.y	. . 3 ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))
2		minvec.x	. . . 4 ⊢ 𝑋 = (Base‘𝑈)
3		eqid 2734	. . . 4 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
4	2, 3	lssss 20907	. . 3 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋)
5	1, 4	syl 17	. 2 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
6		minvec.m	. . . 4 ⊢ − = (-_g‘𝑈)
7		minvec.n	. . . 4 ⊢ 𝑁 = (norm‘𝑈)
8		minvec.u	. . . 4 ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)
9		minvec.w	. . . 4 ⊢ (𝜑 → (𝑈 ↾_s 𝑌) ∈ CMetSp)
10		minvec.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
11		minvec.j	. . . 4 ⊢ 𝐽 = (TopOpen‘𝑈)
12		minvec.r	. . . 4 ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))
13		minvec.s	. . . 4 ⊢ 𝑆 = inf(𝑅, ℝ, < )
14		minvec.d	. . . 4 ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))
15		minvec.f	. . . 4 ⊢ 𝐹 = ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})
16		minvec.p	. . . 4 ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))
17	2, 6, 7, 8, 1, 9, 10, 11, 12, 13, 14, 15, 16	minveclem4a 25419	. . 3 ⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
18	17	elin2d 4187	. 2 ⊢ (𝜑 → 𝑃 ∈ 𝑌)
19	5, 18	sseldd 3966	1 ⊢ (𝜑 → 𝑃 ∈ 𝑋)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2107 {crab 3420 ⊆ wss 3933 ∪ cuni 4889 class class class wbr 5125 ↦ cmpt 5207 × cxp 5665 ran crn 5668 ↾ cres 5669 ‘cfv 6542 (class class class)co 7414 infcinf 9464 ℝcr 11137 + caddc 11141 < clt 11278 ≤ cle 11279 2c2 12304 ℝ⁺crp 13017 ↑cexp 14085 Basecbs 17230 ↾_s cress 17256 distcds 17286 TopOpenctopn 17442 -_gcsg 18927 LSubSpclss 20902 filGencfg 21320 fLim cflim 23907 normcnm 24552 ℂPreHilccph 25155 CMetSpccms 25321

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5261 ax-sep 5278 ax-nul 5288 ax-pow 5347 ax-pr 5414 ax-un 7738 ax-cnex 11194 ax-resscn 11195 ax-1cn 11196 ax-icn 11197 ax-addcl 11198 ax-addrcl 11199 ax-mulcl 11200 ax-mulrcl 11201 ax-mulcom 11202 ax-addass 11203 ax-mulass 11204 ax-distr 11205 ax-i2m1 11206 ax-1ne0 11207 ax-1rid 11208 ax-rnegex 11209 ax-rrecex 11210 ax-cnre 11211 ax-pre-lttri 11212 ax-pre-lttrn 11213 ax-pre-ltadd 11214 ax-pre-mulgt0 11215 ax-pre-sup 11216 ax-addf 11217 ax-mulf 11218

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3773 df-csb 3882 df-dif 3936 df-un 3938 df-in 3940 df-ss 3950 df-pss 3953 df-nul 4316 df-if 4508 df-pw 4584 df-sn 4609 df-pr 4611 df-tp 4613 df-op 4615 df-uni 4890 df-int 4929 df-iun 4975 df-br 5126 df-opab 5188 df-mpt 5208 df-tr 5242 df-id 5560 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5673 df-rel 5674 df-cnv 5675 df-co 5676 df-dm 5677 df-rn 5678 df-res 5679 df-ima 5680 df-pred 6303 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6495 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7871 df-1st 7997 df-2nd 7998 df-tpos 8234 df-frecs 8289 df-wrecs 8320 df-recs 8394 df-rdg 8433 df-1o 8489 df-er 8728 df-map 8851 df-en 8969 df-dom 8970 df-sdom 8971 df-fin 8972 df-fi 9434 df-sup 9465 df-inf 9466 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 df-sub 11477 df-neg 11478 df-div 11904 df-nn 12250 df-2 12312 df-3 12313 df-4 12314 df-5 12315 df-6 12316 df-7 12317 df-8 12318 df-9 12319 df-n0 12511 df-z 12598 df-dec 12718 df-uz 12862 df-q 12974 df-rp 13018 df-xneg 13137 df-xadd 13138 df-xmul 13139 df-ico 13376 df-icc 13377 df-fz 13531 df-seq 14026 df-exp 14086 df-cj 15121 df-re 15122 df-im 15123 df-sqrt 15257 df-abs 15258 df-struct 17167 df-sets 17184 df-slot 17202 df-ndx 17214 df-base 17231 df-ress 17257 df-plusg 17290 df-mulr 17291 df-starv 17292 df-sca 17293 df-vsca 17294 df-ip 17295 df-tset 17296 df-ple 17297 df-ds 17299 df-unif 17300 df-rest 17443 df-0g 17462 df-topgen 17464 df-mgm 18627 df-sgrp 18706 df-mnd 18722 df-mhm 18770 df-grp 18928 df-minusg 18929 df-sbg 18930 df-mulg 19060 df-subg 19115 df-ghm 19205 df-cmn 19773 df-abl 19774 df-mgp 20111 df-rng 20123 df-ur 20152 df-ring 20205 df-cring 20206 df-oppr 20307 df-dvdsr 20330 df-unit 20331 df-invr 20361 df-dvr 20374 df-rhm 20445 df-subrg 20543 df-drng 20704 df-staf 20813 df-srng 20814 df-lmod 20833 df-lss 20903 df-lmhm 20994 df-lvec 21075 df-sra 21145 df-rgmod 21146 df-psmet 21323 df-xmet 21324 df-met 21325 df-bl 21326 df-mopn 21327 df-fbas 21328 df-fg 21329 df-cnfld 21332 df-phl 21611 df-top 22867 df-topon 22884 df-topsp 22906 df-bases 22919 df-ntr 22993 df-nei 23071 df-haus 23288 df-fil 23819 df-flim 23912 df-xms 24294 df-ms 24295 df-nm 24558 df-ngp 24559 df-nlm 24562 df-clm 25051 df-cph 25157 df-cfil 25244 df-cmet 25246 df-cms 25324

This theorem is referenced by: minveclem4 25421

W3C validator