Metamath Proof Explorer

Theorem h2hlm

Description: The limit sequences of Hilbert space. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 13-May-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022) (New usage is discouraged.)

Ref Expression
Hypotheses h2hl.1 ⊒ π‘ˆ = ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩
h2hl.2 ⊒ π‘ˆ ∈ NrmCVec
h2hl.3 ⊒ β„‹ = ( BaseSet β€˜ π‘ˆ )
h2hl.4 ⊒ 𝐷 = ( IndMet β€˜ π‘ˆ )
h2hl.5 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
Assertion h2hlm ⇝𝑣 = ( ( ⇝𝑑 β€˜ 𝐽 ) β†Ύ ( β„‹ ↑m β„• ) )

Proof

Step Hyp Ref Expression
1 h2hl.1 ⊒ π‘ˆ = ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩
2 h2hl.2 ⊒ π‘ˆ ∈ NrmCVec
3 h2hl.3 ⊒ β„‹ = ( BaseSet β€˜ π‘ˆ )
4 h2hl.4 ⊒ 𝐷 = ( IndMet β€˜ π‘ˆ )
5 h2hl.5 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
6 df-hlim ⊒ ⇝𝑣 = { ⟨ 𝑓 , π‘₯ ⟩ ∣ ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘₯ ∈ β„‹ ) ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) }
7 6 relopabiv ⊒ Rel ⇝𝑣
8 relres ⊒ Rel ( ( ⇝𝑑 β€˜ 𝐽 ) β†Ύ ( β„‹ ↑m β„• ) )
9 6 eleq2i ⊒ ( ⟨ 𝑓 , π‘₯ ⟩ ∈ ⇝𝑣 ↔ ⟨ 𝑓 , π‘₯ ⟩ ∈ { ⟨ 𝑓 , π‘₯ ⟩ ∣ ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘₯ ∈ β„‹ ) ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) } )
10 opabidw ⊒ ( ⟨ 𝑓 , π‘₯ ⟩ ∈ { ⟨ 𝑓 , π‘₯ ⟩ ∣ ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘₯ ∈ β„‹ ) ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) } ↔ ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘₯ ∈ β„‹ ) ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) )
11 3 hlex ⊒ β„‹ ∈ V
12 nnex ⊒ β„• ∈ V
13 11 12 elmap ⊒ ( 𝑓 ∈ ( β„‹ ↑m β„• ) ↔ 𝑓 : β„• ⟢ β„‹ )
14 13 anbi1i ⊒ ( ( 𝑓 ∈ ( β„‹ ↑m β„• ) ∧ ⟨ 𝑓 , π‘₯ ⟩ ∈ ( ⇝𝑑 β€˜ 𝐽 ) ) ↔ ( 𝑓 : β„• ⟢ β„‹ ∧ ⟨ 𝑓 , π‘₯ ⟩ ∈ ( ⇝𝑑 β€˜ 𝐽 ) ) )
15 df-br ⊒ ( 𝑓 ( ⇝𝑑 β€˜ 𝐽 ) π‘₯ ↔ ⟨ 𝑓 , π‘₯ ⟩ ∈ ( ⇝𝑑 β€˜ 𝐽 ) )
16 3 4 imsxmet ⊒ ( π‘ˆ ∈ NrmCVec β†’ 𝐷 ∈ ( ∞Met β€˜ β„‹ ) )
17 2 16 mp1i ⊒ ( 𝑓 : β„• ⟢ β„‹ β†’ 𝐷 ∈ ( ∞Met β€˜ β„‹ ) )
18 nnuz ⊒ β„• = ( β„€β‰₯ β€˜ 1 )
19 1zzd ⊒ ( 𝑓 : β„• ⟢ β„‹ β†’ 1 ∈ β„€ )
20 eqidd ⊒ ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘˜ ∈ β„• ) β†’ ( 𝑓 β€˜ π‘˜ ) = ( 𝑓 β€˜ π‘˜ ) )
21 id ⊒ ( 𝑓 : β„• ⟢ β„‹ β†’ 𝑓 : β„• ⟢ β„‹ )
22 5 17 18 19 20 21 lmmbrf ⊒ ( 𝑓 : β„• ⟢ β„‹ β†’ ( 𝑓 ( ⇝𝑑 β€˜ 𝐽 ) π‘₯ ↔ ( π‘₯ ∈ β„‹ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( ( 𝑓 β€˜ π‘˜ ) 𝐷 π‘₯ ) < 𝑦 ) ) )
23 eluznn ⊒ ( ( 𝑗 ∈ β„• ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ) β†’ π‘˜ ∈ β„• )
24 ffvelcdm ⊒ ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘˜ ∈ β„• ) β†’ ( 𝑓 β€˜ π‘˜ ) ∈ β„‹ )
25 1 2 3 4 h2hmetdval ⊒ ( ( ( 𝑓 β€˜ π‘˜ ) ∈ β„‹ ∧ π‘₯ ∈ β„‹ ) β†’ ( ( 𝑓 β€˜ π‘˜ ) 𝐷 π‘₯ ) = ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) )
26 24 25 sylan ⊒ ( ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘˜ ∈ β„• ) ∧ π‘₯ ∈ β„‹ ) β†’ ( ( 𝑓 β€˜ π‘˜ ) 𝐷 π‘₯ ) = ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) )
27 26 breq1d ⊒ ( ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘˜ ∈ β„• ) ∧ π‘₯ ∈ β„‹ ) β†’ ( ( ( 𝑓 β€˜ π‘˜ ) 𝐷 π‘₯ ) < 𝑦 ↔ ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) )
28 27 an32s ⊒ ( ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘₯ ∈ β„‹ ) ∧ π‘˜ ∈ β„• ) β†’ ( ( ( 𝑓 β€˜ π‘˜ ) 𝐷 π‘₯ ) < 𝑦 ↔ ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) )
29 23 28 sylan2 ⊒ ( ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘₯ ∈ β„‹ ) ∧ ( 𝑗 ∈ β„• ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ) ) β†’ ( ( ( 𝑓 β€˜ π‘˜ ) 𝐷 π‘₯ ) < 𝑦 ↔ ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) )
30 29 anassrs ⊒ ( ( ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘₯ ∈ β„‹ ) ∧ 𝑗 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ) β†’ ( ( ( 𝑓 β€˜ π‘˜ ) 𝐷 π‘₯ ) < 𝑦 ↔ ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) )
31 30 ralbidva ⊒ ( ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘₯ ∈ β„‹ ) ∧ 𝑗 ∈ β„• ) β†’ ( βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( ( 𝑓 β€˜ π‘˜ ) 𝐷 π‘₯ ) < 𝑦 ↔ βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) )
32 31 rexbidva ⊒ ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘₯ ∈ β„‹ ) β†’ ( βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( ( 𝑓 β€˜ π‘˜ ) 𝐷 π‘₯ ) < 𝑦 ↔ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) )
33 32 ralbidv ⊒ ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘₯ ∈ β„‹ ) β†’ ( βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( ( 𝑓 β€˜ π‘˜ ) 𝐷 π‘₯ ) < 𝑦 ↔ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) )
34 33 pm5.32da ⊒ ( 𝑓 : β„• ⟢ β„‹ β†’ ( ( π‘₯ ∈ β„‹ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( ( 𝑓 β€˜ π‘˜ ) 𝐷 π‘₯ ) < 𝑦 ) ↔ ( π‘₯ ∈ β„‹ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) ) )
35 22 34 bitrd ⊒ ( 𝑓 : β„• ⟢ β„‹ β†’ ( 𝑓 ( ⇝𝑑 β€˜ 𝐽 ) π‘₯ ↔ ( π‘₯ ∈ β„‹ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) ) )
36 15 35 bitr3id ⊒ ( 𝑓 : β„• ⟢ β„‹ β†’ ( ⟨ 𝑓 , π‘₯ ⟩ ∈ ( ⇝𝑑 β€˜ 𝐽 ) ↔ ( π‘₯ ∈ β„‹ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) ) )
37 36 pm5.32i ⊒ ( ( 𝑓 : β„• ⟢ β„‹ ∧ ⟨ 𝑓 , π‘₯ ⟩ ∈ ( ⇝𝑑 β€˜ 𝐽 ) ) ↔ ( 𝑓 : β„• ⟢ β„‹ ∧ ( π‘₯ ∈ β„‹ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) ) )
38 14 37 bitr2i ⊒ ( ( 𝑓 : β„• ⟢ β„‹ ∧ ( π‘₯ ∈ β„‹ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) ) ↔ ( 𝑓 ∈ ( β„‹ ↑m β„• ) ∧ ⟨ 𝑓 , π‘₯ ⟩ ∈ ( ⇝𝑑 β€˜ 𝐽 ) ) )
39 anass ⊒ ( ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘₯ ∈ β„‹ ) ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) ↔ ( 𝑓 : β„• ⟢ β„‹ ∧ ( π‘₯ ∈ β„‹ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) ) )
40 opelres ⊒ ( π‘₯ ∈ V β†’ ( ⟨ 𝑓 , π‘₯ ⟩ ∈ ( ( ⇝𝑑 β€˜ 𝐽 ) β†Ύ ( β„‹ ↑m β„• ) ) ↔ ( 𝑓 ∈ ( β„‹ ↑m β„• ) ∧ ⟨ 𝑓 , π‘₯ ⟩ ∈ ( ⇝𝑑 β€˜ 𝐽 ) ) ) )
41 40 elv ⊒ ( ⟨ 𝑓 , π‘₯ ⟩ ∈ ( ( ⇝𝑑 β€˜ 𝐽 ) β†Ύ ( β„‹ ↑m β„• ) ) ↔ ( 𝑓 ∈ ( β„‹ ↑m β„• ) ∧ ⟨ 𝑓 , π‘₯ ⟩ ∈ ( ⇝𝑑 β€˜ 𝐽 ) ) )
42 38 39 41 3bitr4i ⊒ ( ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘₯ ∈ β„‹ ) ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ π‘˜ ) βˆ’β„Ž π‘₯ ) ) < 𝑦 ) ↔ ⟨ 𝑓 , π‘₯ ⟩ ∈ ( ( ⇝𝑑 β€˜ 𝐽 ) β†Ύ ( β„‹ ↑m β„• ) ) )
43 9 10 42 3bitri ⊒ ( ⟨ 𝑓 , π‘₯ ⟩ ∈ ⇝𝑣 ↔ ⟨ 𝑓 , π‘₯ ⟩ ∈ ( ( ⇝𝑑 β€˜ 𝐽 ) β†Ύ ( β„‹ ↑m β„• ) ) )
44 7 8 43 eqrelriiv ⊒ ⇝𝑣 = ( ( ⇝𝑑 β€˜ 𝐽 ) β†Ύ ( β„‹ ↑m β„• ) )