Metamath Proof Explorer

Theorem minvecolem4a

Description: Lemma for minveco . F is convergent in the subspace topology on Y . (Contributed by Mario Carneiro, 7-May-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 minvecolem4a ( πœ‘ β†’ 𝐹 ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) )

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 ⊒ ( IndMet β€˜ π‘Š ) = ( IndMet β€˜ π‘Š )
20 eqid ⊒ ( SubSp β€˜ π‘ˆ ) = ( SubSp β€˜ π‘ˆ )
21 4 8 19 20 sspims ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ ( SubSp β€˜ π‘ˆ ) ) β†’ ( IndMet β€˜ π‘Š ) = ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) )
22 15 18 21 syl2anc ⊒ ( πœ‘ β†’ ( IndMet β€˜ π‘Š ) = ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) )
23 17 simprd ⊒ ( πœ‘ β†’ π‘Š ∈ CBan )
24 eqid ⊒ ( BaseSet β€˜ π‘Š ) = ( BaseSet β€˜ π‘Š )
25 24 19 cbncms ⊒ ( π‘Š ∈ CBan β†’ ( IndMet β€˜ π‘Š ) ∈ ( CMet β€˜ ( BaseSet β€˜ π‘Š ) ) )
26 23 25 syl ⊒ ( πœ‘ β†’ ( IndMet β€˜ π‘Š ) ∈ ( CMet β€˜ ( BaseSet β€˜ π‘Š ) ) )
27 22 26 eqeltrrd ⊒ ( πœ‘ β†’ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ∈ ( CMet β€˜ ( BaseSet β€˜ π‘Š ) ) )
28 1 2 3 4 5 6 7 8 9 10 11 12 13 minvecolem3 ⊒ ( πœ‘ β†’ 𝐹 ∈ ( Cau β€˜ 𝐷 ) )
29 1 8 imsmet ⊒ ( π‘ˆ ∈ NrmCVec β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
30 5 14 29 3syl ⊒ ( πœ‘ β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
31 metxmet ⊒ ( 𝐷 ∈ ( Met β€˜ 𝑋 ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
32 30 31 syl ⊒ ( πœ‘ β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
33 causs ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 : β„• ⟢ π‘Œ ) β†’ ( 𝐹 ∈ ( Cau β€˜ 𝐷 ) ↔ 𝐹 ∈ ( Cau β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) )
34 32 12 33 syl2anc ⊒ ( πœ‘ β†’ ( 𝐹 ∈ ( Cau β€˜ 𝐷 ) ↔ 𝐹 ∈ ( Cau β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) )
35 28 34 mpbid ⊒ ( πœ‘ β†’ 𝐹 ∈ ( Cau β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) )
36 eqid ⊒ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) = ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) )
37 36 cmetcau ⊒ ( ( ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ∈ ( CMet β€˜ ( BaseSet β€˜ π‘Š ) ) ∧ 𝐹 ∈ ( Cau β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ 𝐹 ∈ dom ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) )
38 27 35 37 syl2anc ⊒ ( πœ‘ β†’ 𝐹 ∈ dom ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) )
39 xmetres ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ∈ ( ∞Met β€˜ ( 𝑋 ∩ π‘Œ ) ) )
40 36 methaus ⊒ ( ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ∈ ( ∞Met β€˜ ( 𝑋 ∩ π‘Œ ) ) β†’ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ∈ Haus )
41 32 39 40 3syl ⊒ ( πœ‘ β†’ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ∈ Haus )
42 lmfun ⊒ ( ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ∈ Haus β†’ Fun ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) )
43 funfvbrb ⊒ ( Fun ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ ( 𝐹 ∈ dom ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ↔ 𝐹 ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) ) )
44 41 42 43 3syl ⊒ ( πœ‘ β†’ ( 𝐹 ∈ dom ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ↔ 𝐹 ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) ) )
45 38 44 mpbid ⊒ ( πœ‘ β†’ 𝐹 ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) )