Theorem minveclem4b

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

	Ref	Expression
Hypotheses	minvec.x	|- X = ( Base ` U )
	minvec.m	|- .- = ( -g ` U )
	minvec.n	|- N = ( norm ` U )
	minvec.u	|- ( ph -> U e. CPreHil )
	minvec.y	|- ( ph -> Y e. ( LSubSp ` U ) )
	minvec.w	|- ( ph -> ( U |`s Y ) e. CMetSp )
	minvec.a	|- ( ph -> A e. X )
	minvec.j	|- J = ( TopOpen ` U )
	minvec.r	|- R = ran ( y e. Y |-> ( N ` ( A .- y ) ) )
	minvec.s	|- S = inf ( R , RR , < )
	minvec.d	|- D = ( ( dist ` U ) |` ( X X. X ) )
	minvec.f	|- F = ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
	minvec.p	|- P = U. ( J fLim ( X filGen F ) )
Assertion	minveclem4b	|- ( ph -> P e. X )

Proof

Step	Hyp	Ref	Expression
1		minvec.x	|- X = ( Base ` U )
2		minvec.m	|- .- = ( -g ` U )
3		minvec.n	|- N = ( norm ` U )
4		minvec.u	|- ( ph -> U e. CPreHil )
5		minvec.y	|- ( ph -> Y e. ( LSubSp ` U ) )
6		minvec.w	|- ( ph -> ( U |`s Y ) e. CMetSp )
7		minvec.a	|- ( ph -> A e. X )
8		minvec.j	|- J = ( TopOpen ` U )
9		minvec.r	|- R = ran ( y e. Y |-> ( N ` ( A .- y ) ) )
10		minvec.s	|- S = inf ( R , RR , < )
11		minvec.d	|- D = ( ( dist ` U ) |` ( X X. X ) )
12		minvec.f	|- F = ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
13		minvec.p	|- P = U. ( J fLim ( X filGen F ) )
14		eqid	|- ( LSubSp ` U ) = ( LSubSp ` U )
15	1 14	lssss	|- ( Y e. ( LSubSp ` U ) -> Y C_ X )
16	5 15	syl	|- ( ph -> Y C_ X )
17	1 2 3 4 5 6 7 8 9 10 11 12 13	minveclem4a	|- ( ph -> P e. ( ( J fLim ( X filGen F ) ) i^i Y ) )
18	17	elin2d	|- ( ph -> P e. Y )
19	16 18	sseldd	|- ( ph -> P e. X )