Metamath Proof Explorer

Theorem minveclem4a

Description: Lemma for minvec . F converges to a point P in Y . (Contributed by Mario Carneiro, 7-May-2014) (Revised by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses 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 minveclem4a ( πœ‘ β†’ 𝑃 ∈ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) )

Proof

Step Hyp Ref Expression
1 minvec.x ⊒ 𝑋 = ( Base β€˜ π‘ˆ )
2 minvec.m ⊒ βˆ’ = ( -g β€˜ π‘ˆ )
3 minvec.n ⊒ 𝑁 = ( norm β€˜ π‘ˆ )
4 minvec.u ⊒ ( πœ‘ β†’ π‘ˆ ∈ β„‚PreHil )
5 minvec.y ⊒ ( πœ‘ β†’ π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) )
6 minvec.w ⊒ ( πœ‘ β†’ ( π‘ˆ β†Ύs π‘Œ ) ∈ CMetSp )
7 minvec.a ⊒ ( πœ‘ β†’ 𝐴 ∈ 𝑋 )
8 minvec.j ⊒ 𝐽 = ( TopOpen β€˜ π‘ˆ )
9 minvec.r ⊒ 𝑅 = ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
10 minvec.s ⊒ 𝑆 = inf ( 𝑅 , ℝ , < )
11 minvec.d ⊒ 𝐷 = ( ( dist β€˜ π‘ˆ ) β†Ύ ( 𝑋 Γ— 𝑋 ) )
12 minvec.f ⊒ 𝐹 = ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } )
13 minvec.p ⊒ 𝑃 = βˆͺ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) )
14 ovex ⊒ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∈ V
15 14 uniex ⊒ βˆͺ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∈ V
16 15 snid ⊒ βˆͺ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∈ { βˆͺ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) }
17 cphngp ⊒ ( π‘ˆ ∈ β„‚PreHil β†’ π‘ˆ ∈ NrmGrp )
18 ngpxms ⊒ ( π‘ˆ ∈ NrmGrp β†’ π‘ˆ ∈ ∞MetSp )
19 4 17 18 3syl ⊒ ( πœ‘ β†’ π‘ˆ ∈ ∞MetSp )
20 8 1 11 xmstopn ⊒ ( π‘ˆ ∈ ∞MetSp β†’ 𝐽 = ( MetOpen β€˜ 𝐷 ) )
21 19 20 syl ⊒ ( πœ‘ β†’ 𝐽 = ( MetOpen β€˜ 𝐷 ) )
22 21 oveq1d ⊒ ( πœ‘ β†’ ( 𝐽 β†Ύt π‘Œ ) = ( ( MetOpen β€˜ 𝐷 ) β†Ύt π‘Œ ) )
23 1 11 xmsxmet ⊒ ( π‘ˆ ∈ ∞MetSp β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
24 19 23 syl ⊒ ( πœ‘ β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
25 eqid ⊒ ( LSubSp β€˜ π‘ˆ ) = ( LSubSp β€˜ π‘ˆ )
26 1 25 lssss ⊒ ( π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) β†’ π‘Œ βŠ† 𝑋 )
27 5 26 syl ⊒ ( πœ‘ β†’ π‘Œ βŠ† 𝑋 )
28 eqid ⊒ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) = ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) )
29 eqid ⊒ ( MetOpen β€˜ 𝐷 ) = ( MetOpen β€˜ 𝐷 )
30 eqid ⊒ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) = ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) )
31 28 29 30 metrest ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( ( MetOpen β€˜ 𝐷 ) β†Ύt π‘Œ ) = ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) )
32 24 27 31 syl2anc ⊒ ( πœ‘ β†’ ( ( MetOpen β€˜ 𝐷 ) β†Ύt π‘Œ ) = ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) )
33 22 32 eqtr2d ⊒ ( πœ‘ β†’ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) = ( 𝐽 β†Ύt π‘Œ ) )
34 1 2 3 4 5 6 7 8 9 10 11 12 minveclem3b ⊒ ( πœ‘ β†’ 𝐹 ∈ ( fBas β€˜ π‘Œ ) )
35 fgcl ⊒ ( 𝐹 ∈ ( fBas β€˜ π‘Œ ) β†’ ( π‘Œ filGen 𝐹 ) ∈ ( Fil β€˜ π‘Œ ) )
36 34 35 syl ⊒ ( πœ‘ β†’ ( π‘Œ filGen 𝐹 ) ∈ ( Fil β€˜ π‘Œ ) )
37 1 fvexi ⊒ 𝑋 ∈ V
38 37 a1i ⊒ ( πœ‘ β†’ 𝑋 ∈ V )
39 trfg ⊒ ( ( ( π‘Œ filGen 𝐹 ) ∈ ( Fil β€˜ π‘Œ ) ∧ π‘Œ βŠ† 𝑋 ∧ 𝑋 ∈ V ) β†’ ( ( 𝑋 filGen ( π‘Œ filGen 𝐹 ) ) β†Ύt π‘Œ ) = ( π‘Œ filGen 𝐹 ) )
40 36 27 38 39 syl3anc ⊒ ( πœ‘ β†’ ( ( 𝑋 filGen ( π‘Œ filGen 𝐹 ) ) β†Ύt π‘Œ ) = ( π‘Œ filGen 𝐹 ) )
41 fgabs ⊒ ( ( 𝐹 ∈ ( fBas β€˜ π‘Œ ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( 𝑋 filGen ( π‘Œ filGen 𝐹 ) ) = ( 𝑋 filGen 𝐹 ) )
42 34 27 41 syl2anc ⊒ ( πœ‘ β†’ ( 𝑋 filGen ( π‘Œ filGen 𝐹 ) ) = ( 𝑋 filGen 𝐹 ) )
43 42 oveq1d ⊒ ( πœ‘ β†’ ( ( 𝑋 filGen ( π‘Œ filGen 𝐹 ) ) β†Ύt π‘Œ ) = ( ( 𝑋 filGen 𝐹 ) β†Ύt π‘Œ ) )
44 40 43 eqtr3d ⊒ ( πœ‘ β†’ ( π‘Œ filGen 𝐹 ) = ( ( 𝑋 filGen 𝐹 ) β†Ύt π‘Œ ) )
45 33 44 oveq12d ⊒ ( πœ‘ β†’ ( ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) fLim ( π‘Œ filGen 𝐹 ) ) = ( ( 𝐽 β†Ύt π‘Œ ) fLim ( ( 𝑋 filGen 𝐹 ) β†Ύt π‘Œ ) ) )
46 xmstps ⊒ ( π‘ˆ ∈ ∞MetSp β†’ π‘ˆ ∈ TopSp )
47 19 46 syl ⊒ ( πœ‘ β†’ π‘ˆ ∈ TopSp )
48 1 8 istps ⊒ ( π‘ˆ ∈ TopSp ↔ 𝐽 ∈ ( TopOn β€˜ 𝑋 ) )
49 47 48 sylib ⊒ ( πœ‘ β†’ 𝐽 ∈ ( TopOn β€˜ 𝑋 ) )
50 fbsspw ⊒ ( 𝐹 ∈ ( fBas β€˜ π‘Œ ) β†’ 𝐹 βŠ† 𝒫 π‘Œ )
51 34 50 syl ⊒ ( πœ‘ β†’ 𝐹 βŠ† 𝒫 π‘Œ )
52 27 sspwd ⊒ ( πœ‘ β†’ 𝒫 π‘Œ βŠ† 𝒫 𝑋 )
53 51 52 sstrd ⊒ ( πœ‘ β†’ 𝐹 βŠ† 𝒫 𝑋 )
54 fbasweak ⊒ ( ( 𝐹 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 βŠ† 𝒫 𝑋 ∧ 𝑋 ∈ V ) β†’ 𝐹 ∈ ( fBas β€˜ 𝑋 ) )
55 34 53 38 54 syl3anc ⊒ ( πœ‘ β†’ 𝐹 ∈ ( fBas β€˜ 𝑋 ) )
56 fgcl ⊒ ( 𝐹 ∈ ( fBas β€˜ 𝑋 ) β†’ ( 𝑋 filGen 𝐹 ) ∈ ( Fil β€˜ 𝑋 ) )
57 55 56 syl ⊒ ( πœ‘ β†’ ( 𝑋 filGen 𝐹 ) ∈ ( Fil β€˜ 𝑋 ) )
58 filfbas ⊒ ( ( π‘Œ filGen 𝐹 ) ∈ ( Fil β€˜ π‘Œ ) β†’ ( π‘Œ filGen 𝐹 ) ∈ ( fBas β€˜ π‘Œ ) )
59 34 35 58 3syl ⊒ ( πœ‘ β†’ ( π‘Œ filGen 𝐹 ) ∈ ( fBas β€˜ π‘Œ ) )
60 fbsspw ⊒ ( ( π‘Œ filGen 𝐹 ) ∈ ( fBas β€˜ π‘Œ ) β†’ ( π‘Œ filGen 𝐹 ) βŠ† 𝒫 π‘Œ )
61 59 60 syl ⊒ ( πœ‘ β†’ ( π‘Œ filGen 𝐹 ) βŠ† 𝒫 π‘Œ )
62 61 52 sstrd ⊒ ( πœ‘ β†’ ( π‘Œ filGen 𝐹 ) βŠ† 𝒫 𝑋 )
63 fbasweak ⊒ ( ( ( π‘Œ filGen 𝐹 ) ∈ ( fBas β€˜ π‘Œ ) ∧ ( π‘Œ filGen 𝐹 ) βŠ† 𝒫 𝑋 ∧ 𝑋 ∈ V ) β†’ ( π‘Œ filGen 𝐹 ) ∈ ( fBas β€˜ 𝑋 ) )
64 59 62 38 63 syl3anc ⊒ ( πœ‘ β†’ ( π‘Œ filGen 𝐹 ) ∈ ( fBas β€˜ 𝑋 ) )
65 ssfg ⊒ ( ( π‘Œ filGen 𝐹 ) ∈ ( fBas β€˜ 𝑋 ) β†’ ( π‘Œ filGen 𝐹 ) βŠ† ( 𝑋 filGen ( π‘Œ filGen 𝐹 ) ) )
66 64 65 syl ⊒ ( πœ‘ β†’ ( π‘Œ filGen 𝐹 ) βŠ† ( 𝑋 filGen ( π‘Œ filGen 𝐹 ) ) )
67 66 42 sseqtrd ⊒ ( πœ‘ β†’ ( π‘Œ filGen 𝐹 ) βŠ† ( 𝑋 filGen 𝐹 ) )
68 filtop ⊒ ( ( π‘Œ filGen 𝐹 ) ∈ ( Fil β€˜ π‘Œ ) β†’ π‘Œ ∈ ( π‘Œ filGen 𝐹 ) )
69 36 68 syl ⊒ ( πœ‘ β†’ π‘Œ ∈ ( π‘Œ filGen 𝐹 ) )
70 67 69 sseldd ⊒ ( πœ‘ β†’ π‘Œ ∈ ( 𝑋 filGen 𝐹 ) )
71 flimrest ⊒ ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ ( 𝑋 filGen 𝐹 ) ∈ ( Fil β€˜ 𝑋 ) ∧ π‘Œ ∈ ( 𝑋 filGen 𝐹 ) ) β†’ ( ( 𝐽 β†Ύt π‘Œ ) fLim ( ( 𝑋 filGen 𝐹 ) β†Ύt π‘Œ ) ) = ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) )
72 49 57 70 71 syl3anc ⊒ ( πœ‘ β†’ ( ( 𝐽 β†Ύt π‘Œ ) fLim ( ( 𝑋 filGen 𝐹 ) β†Ύt π‘Œ ) ) = ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) )
73 45 72 eqtrd ⊒ ( πœ‘ β†’ ( ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) fLim ( π‘Œ filGen 𝐹 ) ) = ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) )
74 1 2 3 4 5 6 7 8 9 10 11 minveclem3a ⊒ ( πœ‘ β†’ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ∈ ( CMet β€˜ π‘Œ ) )
75 1 2 3 4 5 6 7 8 9 10 11 12 minveclem3 ⊒ ( πœ‘ β†’ ( π‘Œ filGen 𝐹 ) ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) )
76 30 cmetcvg ⊒ ( ( ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ∈ ( CMet β€˜ π‘Œ ) ∧ ( π‘Œ filGen 𝐹 ) ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ ( ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) fLim ( π‘Œ filGen 𝐹 ) ) β‰  βˆ… )
77 74 75 76 syl2anc ⊒ ( πœ‘ β†’ ( ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) fLim ( π‘Œ filGen 𝐹 ) ) β‰  βˆ… )
78 73 77 eqnetrrd ⊒ ( πœ‘ β†’ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) β‰  βˆ… )
79 78 neneqd ⊒ ( πœ‘ β†’ Β¬ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) = βˆ… )
80 inss1 ⊒ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) βŠ† ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) )
81 29 methaus ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( MetOpen β€˜ 𝐷 ) ∈ Haus )
82 23 81 syl ⊒ ( π‘ˆ ∈ ∞MetSp β†’ ( MetOpen β€˜ 𝐷 ) ∈ Haus )
83 20 82 eqeltrd ⊒ ( π‘ˆ ∈ ∞MetSp β†’ 𝐽 ∈ Haus )
84 hausflimi ⊒ ( 𝐽 ∈ Haus β†’ βˆƒ* π‘₯ π‘₯ ∈ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) )
85 19 83 84 3syl ⊒ ( πœ‘ β†’ βˆƒ* π‘₯ π‘₯ ∈ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) )
86 ssn0 ⊒ ( ( ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) βŠ† ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∧ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) β‰  βˆ… ) β†’ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) β‰  βˆ… )
87 80 78 86 sylancr ⊒ ( πœ‘ β†’ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) β‰  βˆ… )
88 n0moeu ⊒ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) β‰  βˆ… β†’ ( βˆƒ* π‘₯ π‘₯ ∈ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ↔ βˆƒ! π‘₯ π‘₯ ∈ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ) )
89 87 88 syl ⊒ ( πœ‘ β†’ ( βˆƒ* π‘₯ π‘₯ ∈ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ↔ βˆƒ! π‘₯ π‘₯ ∈ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ) )
90 85 89 mpbid ⊒ ( πœ‘ β†’ βˆƒ! π‘₯ π‘₯ ∈ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) )
91 euen1b ⊒ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) β‰ˆ 1o ↔ βˆƒ! π‘₯ π‘₯ ∈ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) )
92 90 91 sylibr ⊒ ( πœ‘ β†’ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) β‰ˆ 1o )
93 en1b ⊒ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) β‰ˆ 1o ↔ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) = { βˆͺ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) } )
94 92 93 sylib ⊒ ( πœ‘ β†’ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) = { βˆͺ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) } )
95 80 94 sseqtrid ⊒ ( πœ‘ β†’ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) βŠ† { βˆͺ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) } )
96 sssn ⊒ ( ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) βŠ† { βˆͺ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) } ↔ ( ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) = βˆ… ∨ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) = { βˆͺ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) } ) )
97 95 96 sylib ⊒ ( πœ‘ β†’ ( ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) = βˆ… ∨ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) = { βˆͺ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) } ) )
98 97 ord ⊒ ( πœ‘ β†’ ( Β¬ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) = βˆ… β†’ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) = { βˆͺ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) } ) )
99 79 98 mpd ⊒ ( πœ‘ β†’ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) = { βˆͺ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) } )
100 16 99 eleqtrrid ⊒ ( πœ‘ β†’ βˆͺ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∈ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) )
101 13 100 eqeltrid ⊒ ( πœ‘ β†’ 𝑃 ∈ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) )