Metamath Proof Explorer

Theorem hlim0

Description: The zero sequence in Hilbert space converges to the zero vector. (Contributed by NM, 17-Aug-1999) (Proof shortened by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hlim0 ( ℕ × { 0ℎ } ) ⇝𝑣 0ℎ

Proof

Step Hyp Ref Expression
1 ax-hv0cl ⊢ 0ℎ ∈ ℋ
2 1 fconst6 ⊢ ( ℕ × { 0ℎ } ) : ℕ ⟶ ℋ
3 ax-hilex ⊢ ℋ ∈ V
4 nnex ⊢ ℕ ∈ V
5 3 4 elmap ⊢ ( ( ℕ × { 0ℎ } ) ∈ ( ℋ ↑m ℕ ) ↔ ( ℕ × { 0ℎ } ) : ℕ ⟶ ℋ )
6 2 5 mpbir ⊢ ( ℕ × { 0ℎ } ) ∈ ( ℋ ↑m ℕ )
7 eqid ⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
8 eqid ⊢ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
9 7 8 hhxmet ⊢ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ∈ ( ∞Met ‘ ℋ )
10 eqid ⊢ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) = ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) )
11 10 mopntopon ⊢ ( ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ∈ ( ∞Met ‘ ℋ ) → ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ∈ ( TopOn ‘ ℋ ) )
12 9 11 ax-mp ⊢ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ∈ ( TopOn ‘ ℋ )
13 1z ⊢ 1 ∈ ℤ
14 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
15 14 lmconst ⊢ ( ( ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ∈ ( TopOn ‘ ℋ ) ∧ 0ℎ ∈ ℋ ∧ 1 ∈ ℤ ) → ( ℕ × { 0ℎ } ) ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) 0ℎ )
16 12 1 13 15 mp3an ⊢ ( ℕ × { 0ℎ } ) ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) 0ℎ
17 7 8 10 hhlm ⊢ ⇝𝑣 = ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) ↾ ( ℋ ↑m ℕ ) )
18 17 breqi ⊢ ( ( ℕ × { 0ℎ } ) ⇝𝑣 0ℎ ↔ ( ℕ × { 0ℎ } ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) ↾ ( ℋ ↑m ℕ ) ) 0ℎ )
19 1 elexi ⊢ 0ℎ ∈ V
20 19 brresi ⊢ ( ( ℕ × { 0ℎ } ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) ↾ ( ℋ ↑m ℕ ) ) 0ℎ ↔ ( ( ℕ × { 0ℎ } ) ∈ ( ℋ ↑m ℕ ) ∧ ( ℕ × { 0ℎ } ) ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) 0ℎ ) )
21 18 20 bitri ⊢ ( ( ℕ × { 0ℎ } ) ⇝𝑣 0ℎ ↔ ( ( ℕ × { 0ℎ } ) ∈ ( ℋ ↑m ℕ ) ∧ ( ℕ × { 0ℎ } ) ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) 0ℎ ) )
22 6 16 21 mpbir2an ⊢ ( ℕ × { 0ℎ } ) ⇝𝑣 0ℎ