Theorem hhlm

Description: The limit sequences of Hilbert space. (Contributed by NM, 19-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhlm.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
	hhlm.2	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
	hhlm.3	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion	hhlm	⊢ ⇝𝑣 = ( ( ⇝𝑡 ‘ 𝐽 ) ↾ ( ℋ ↑m ℕ ) )

Proof

Step	Hyp	Ref	Expression
1		hhlm.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2		hhlm.2	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
3		hhlm.3	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
4	1	hhnv	⊢ 𝑈 ∈ NrmCVec
5	1	hhba	⊢ ℋ = ( BaseSet ‘ 𝑈 )
6	1 4 5 2 3	h2hlm	⊢ ⇝𝑣 = ( ( ⇝𝑡 ‘ 𝐽 ) ↾ ( ℋ ↑m ℕ ) )