Metamath Proof Explorer

Theorem h2hcau

Description: The Cauchy sequences of Hilbert space. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 13-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses h2hc.1 ⊢U=+ℎ⋅ℎnormℎ
h2hc.2 ⊢U∈NrmCVec
h2hc.3 ⊢ℋ=BaseSet⁡U
h2hc.4 ⊢D=IndMet⁡U
Assertion h2hcau ⊢Cauchy=Cau⁡D∩ℋℕ

Proof

Step Hyp Ref Expression
1 h2hc.1 ⊢U=+ℎ⋅ℎnormℎ
2 h2hc.2 ⊢U∈NrmCVec
3 h2hc.3 ⊢ℋ=BaseSet⁡U
4 h2hc.4 ⊢D=IndMet⁡U
5 df-rab ⊢f∈ℋℕ|∀x∈ℝ+∃j∈ℕ∀k∈ℤ≥jnormℎ⁡f⁡j-ℎf⁡k<x=f|f∈ℋℕ∧∀x∈ℝ+∃j∈ℕ∀k∈ℤ≥jnormℎ⁡f⁡j-ℎf⁡k<x
6 df-hcau ⊢Cauchy=f∈ℋℕ|∀x∈ℝ+∃j∈ℕ∀k∈ℤ≥jnormℎ⁡f⁡j-ℎf⁡k<x
7 elin ⊢f∈Cau⁡D∩ℋℕ↔f∈Cau⁡D∧f∈ℋℕ
8 ancom ⊢f∈Cau⁡D∧f∈ℋℕ↔f∈ℋℕ∧f∈Cau⁡D
9 3 hlex ⊢ℋ∈V
10 nnex ⊢ℕ∈V
11 9 10 elmap ⊢f∈ℋℕ↔f:ℕ⟶ℋ
12 nnuz ⊢ℕ=ℤ≥1
13 3 4 imsxmet ⊢U∈NrmCVec→D∈∞Met⁡ℋ
14 2 13 mp1i ⊢f:ℕ⟶ℋ→D∈∞Met⁡ℋ
15 1zzd ⊢f:ℕ⟶ℋ→1∈ℤ
16 eqidd ⊢f:ℕ⟶ℋ∧k∈ℕ→f⁡k=f⁡k
17 eqidd ⊢f:ℕ⟶ℋ∧j∈ℕ→f⁡j=f⁡j
18 id ⊢f:ℕ⟶ℋ→f:ℕ⟶ℋ
19 12 14 15 16 17 18 iscauf ⊢f:ℕ⟶ℋ→f∈Cau⁡D↔∀x∈ℝ+∃j∈ℕ∀k∈ℤ≥jf⁡jDf⁡k<x
20 ffvelcdm ⊢f:ℕ⟶ℋ∧j∈ℕ→f⁡j∈ℋ
21 20 adantr ⊢f:ℕ⟶ℋ∧j∈ℕ∧k∈ℤ≥j→f⁡j∈ℋ
22 eluznn ⊢j∈ℕ∧k∈ℤ≥j→k∈ℕ
23 ffvelcdm ⊢f:ℕ⟶ℋ∧k∈ℕ→f⁡k∈ℋ
24 22 23 sylan2 ⊢f:ℕ⟶ℋ∧j∈ℕ∧k∈ℤ≥j→f⁡k∈ℋ
25 24 anassrs ⊢f:ℕ⟶ℋ∧j∈ℕ∧k∈ℤ≥j→f⁡k∈ℋ
26 1 2 3 4 h2hmetdval ⊢f⁡j∈ℋ∧f⁡k∈ℋ→f⁡jDf⁡k=normℎ⁡f⁡j-ℎf⁡k
27 21 25 26 syl2anc ⊢f:ℕ⟶ℋ∧j∈ℕ∧k∈ℤ≥j→f⁡jDf⁡k=normℎ⁡f⁡j-ℎf⁡k
28 27 breq1d ⊢f:ℕ⟶ℋ∧j∈ℕ∧k∈ℤ≥j→f⁡jDf⁡k<x↔normℎ⁡f⁡j-ℎf⁡k<x
29 28 ralbidva ⊢f:ℕ⟶ℋ∧j∈ℕ→∀k∈ℤ≥jf⁡jDf⁡k<x↔∀k∈ℤ≥jnormℎ⁡f⁡j-ℎf⁡k<x
30 29 rexbidva ⊢f:ℕ⟶ℋ→∃j∈ℕ∀k∈ℤ≥jf⁡jDf⁡k<x↔∃j∈ℕ∀k∈ℤ≥jnormℎ⁡f⁡j-ℎf⁡k<x
31 30 ralbidv ⊢f:ℕ⟶ℋ→∀x∈ℝ+∃j∈ℕ∀k∈ℤ≥jf⁡jDf⁡k<x↔∀x∈ℝ+∃j∈ℕ∀k∈ℤ≥jnormℎ⁡f⁡j-ℎf⁡k<x
32 19 31 bitrd ⊢f:ℕ⟶ℋ→f∈Cau⁡D↔∀x∈ℝ+∃j∈ℕ∀k∈ℤ≥jnormℎ⁡f⁡j-ℎf⁡k<x
33 11 32 sylbi ⊢f∈ℋℕ→f∈Cau⁡D↔∀x∈ℝ+∃j∈ℕ∀k∈ℤ≥jnormℎ⁡f⁡j-ℎf⁡k<x
34 33 pm5.32i ⊢f∈ℋℕ∧f∈Cau⁡D↔f∈ℋℕ∧∀x∈ℝ+∃j∈ℕ∀k∈ℤ≥jnormℎ⁡f⁡j-ℎf⁡k<x
35 7 8 34 3bitri ⊢f∈Cau⁡D∩ℋℕ↔f∈ℋℕ∧∀x∈ℝ+∃j∈ℕ∀k∈ℤ≥jnormℎ⁡f⁡j-ℎf⁡k<x
36 35 eqabi ⊢Cau⁡D∩ℋℕ=f|f∈ℋℕ∧∀x∈ℝ+∃j∈ℕ∀k∈ℤ≥jnormℎ⁡f⁡j-ℎf⁡k<x
37 5 6 36 3eqtr4i ⊢Cauchy=Cau⁡D∩ℋℕ