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 𝐹 ) ) ∩ 𝑌 ) )