This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hlimcaui

Description: If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence. (Contributed by NM, 17-Aug-1999) (Proof shortened by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hlimcaui ( 𝐹 ⇝𝑣 𝐴 → 𝐹 ∈ Cauchy )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2 eqid ⊢ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
3 eqid ⊢ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) = ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) )
4 1 2 3 hhlm ⊢ ⇝𝑣 = ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) ↾ ( ℋ ↑m ℕ ) )
5 resss ⊢ ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) ↾ ( ℋ ↑m ℕ ) ) ⊆ ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) )
6 4 5 eqsstri ⊢ ⇝𝑣 ⊆ ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) )
7 dmss ⊢ ( ⇝𝑣 ⊆ ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) → dom ⇝𝑣 ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) )
8 6 7 ax-mp ⊢ dom ⇝𝑣 ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) )
9 1 2 hhxmet ⊢ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ∈ ( ∞Met ‘ ℋ )
10 3 lmcau ⊢ ( ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ∈ ( ∞Met ‘ ℋ ) → dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) ⊆ ( Cau ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) )
11 9 10 ax-mp ⊢ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) ⊆ ( Cau ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) )
12 8 11 sstri ⊢ dom ⇝𝑣 ⊆ ( Cau ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) )
13 4 dmeqi ⊢ dom ⇝𝑣 = dom ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) ↾ ( ℋ ↑m ℕ ) )
14 dmres ⊢ dom ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) ↾ ( ℋ ↑m ℕ ) ) = ( ( ℋ ↑m ℕ ) ∩ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) )
15 13 14 eqtri ⊢ dom ⇝𝑣 = ( ( ℋ ↑m ℕ ) ∩ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) )
16 inss1 ⊢ ( ( ℋ ↑m ℕ ) ∩ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) ) ⊆ ( ℋ ↑m ℕ )
17 15 16 eqsstri ⊢ dom ⇝𝑣 ⊆ ( ℋ ↑m ℕ )
18 12 17 ssini ⊢ dom ⇝𝑣 ⊆ ( ( Cau ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ∩ ( ℋ ↑m ℕ ) )
19 1 2 hhcau ⊢ Cauchy = ( ( Cau ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ∩ ( ℋ ↑m ℕ ) )
20 18 19 sseqtrri ⊢ dom ⇝𝑣 ⊆ Cauchy
21 relres ⊢ Rel ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) ↾ ( ℋ ↑m ℕ ) )
22 4 releqi ⊢ ( Rel ⇝𝑣 ↔ Rel ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) ) ↾ ( ℋ ↑m ℕ ) ) )
23 21 22 mpbir ⊢ Rel ⇝𝑣
24 23 releldmi ⊢ ( 𝐹 ⇝𝑣 𝐴 → 𝐹 ∈ dom ⇝𝑣 )
25 20 24 sselid ⊢ ( 𝐹 ⇝𝑣 𝐴 → 𝐹 ∈ Cauchy )