Theorem minvecolem4b

Description: Lemma for minveco . The convergent point of the Cauchy sequence F is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	minveco.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	minveco.m	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
	minveco.n	⊢ 𝑁 = ( normCV ‘ 𝑈 )
	minveco.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	minveco.u	⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
	minveco.w	⊢ ( 𝜑 → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
	minveco.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
	minveco.d	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
	minveco.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	minveco.r	⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
	minveco.s	⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
	minveco.f	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑌 )
	minveco.1	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
Assertion	minvecolem4b	⊢ ( 𝜑 → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		minveco.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		minveco.m	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3		minveco.n	⊢ 𝑁 = ( normCV ‘ 𝑈 )
4		minveco.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
5		minveco.u	⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
6		minveco.w	⊢ ( 𝜑 → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
7		minveco.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8		minveco.d	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
9		minveco.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
10		minveco.r	⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
11		minveco.s	⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
12		minveco.f	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑌 )
13		minveco.1	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
14		phnv	⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )
15	5 14	syl	⊢ ( 𝜑 → 𝑈 ∈ NrmCVec )
16		elin	⊢ ( 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) ↔ ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝑊 ∈ CBan ) )
17	6 16	sylib	⊢ ( 𝜑 → ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝑊 ∈ CBan ) )
18	17	simpld	⊢ ( 𝜑 → 𝑊 ∈ ( SubSp ‘ 𝑈 ) )
19		eqid	⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
20	1 4 19	sspba	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → 𝑌 ⊆ 𝑋 )
21	15 18 20	syl2anc	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
22	1 8	imsxmet	⊢ ( 𝑈 ∈ NrmCVec → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
23	15 22	syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
24	9	methaus	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Haus )
25	23 24	syl	⊢ ( 𝜑 → 𝐽 ∈ Haus )
26		lmfun	⊢ ( 𝐽 ∈ Haus → Fun ( ⇝𝑡 ‘ 𝐽 ) )
27	25 26	syl	⊢ ( 𝜑 → Fun ( ⇝𝑡 ‘ 𝐽 ) )
28	1 2 3 4 5 6 7 8 9 10 11 12 13	minvecolem4a	⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) )
29		eqid	⊢ ( 𝐽 ↾t 𝑌 ) = ( 𝐽 ↾t 𝑌 )
30		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
31	4	fvexi	⊢ 𝑌 ∈ V
32	31	a1i	⊢ ( 𝜑 → 𝑌 ∈ V )
33	9	mopntop	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
34	23 33	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
35		xmetres2	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) )
36	23 21 35	syl2anc	⊢ ( 𝜑 → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) )
37		eqid	⊢ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) )
38	37	mopntopon	⊢ ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) → ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ∈ ( TopOn ‘ 𝑌 ) )
39	36 38	syl	⊢ ( 𝜑 → ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ∈ ( TopOn ‘ 𝑌 ) )
40		lmcl	⊢ ( ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) → ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ∈ 𝑌 )
41	39 28 40	syl2anc	⊢ ( 𝜑 → ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ∈ 𝑌 )
42		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
43	29 30 32 34 41 42 12	lmss	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ↔ 𝐹 ( ⇝𝑡 ‘ ( 𝐽 ↾t 𝑌 ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) )
44		eqid	⊢ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) = ( 𝐷 ↾ ( 𝑌 × 𝑌 ) )
45	44 9 37	metrest	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑌 ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) )
46	23 21 45	syl2anc	⊢ ( 𝜑 → ( 𝐽 ↾t 𝑌 ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) )
47	46	fveq2d	⊢ ( 𝜑 → ( ⇝𝑡 ‘ ( 𝐽 ↾t 𝑌 ) ) = ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )
48	47	breqd	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( 𝐽 ↾t 𝑌 ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ↔ 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) )
49	43 48	bitrd	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ↔ 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) )
50	28 49	mpbird	⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) )
51		funbrfv	⊢ ( Fun ( ⇝𝑡 ‘ 𝐽 ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) )
52	27 50 51	sylc	⊢ ( 𝜑 → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) )
53	52 41	eqeltrd	⊢ ( 𝜑 → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝑌 )
54	21 53	sseldd	⊢ ( 𝜑 → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝑋 )