Metamath Proof Explorer


Theorem hcau

Description: Member of the set of Cauchy sequences on a Hilbert space. Definition for Cauchy sequence in Beran p. 96. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hcau ( 𝐹 ∈ Cauchy ↔ ( 𝐹 : ℕ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥 ) )

Proof

Step Hyp Ref Expression
1 fveq1 ( 𝑓 = 𝐹 → ( 𝑓𝑦 ) = ( 𝐹𝑦 ) )
2 fveq1 ( 𝑓 = 𝐹 → ( 𝑓𝑧 ) = ( 𝐹𝑧 ) )
3 1 2 oveq12d ( 𝑓 = 𝐹 → ( ( 𝑓𝑦 ) − ( 𝑓𝑧 ) ) = ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) )
4 3 fveq2d ( 𝑓 = 𝐹 → ( norm ‘ ( ( 𝑓𝑦 ) − ( 𝑓𝑧 ) ) ) = ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) )
5 4 breq1d ( 𝑓 = 𝐹 → ( ( norm ‘ ( ( 𝑓𝑦 ) − ( 𝑓𝑧 ) ) ) < 𝑥 ↔ ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥 ) )
6 5 rexralbidv ( 𝑓 = 𝐹 → ( ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑦 ) − ( 𝑓𝑧 ) ) ) < 𝑥 ↔ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥 ) )
7 6 ralbidv ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑦 ) − ( 𝑓𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥 ) )
8 df-hcau Cauchy = { 𝑓 ∈ ( ℋ ↑m ℕ ) ∣ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑦 ) − ( 𝑓𝑧 ) ) ) < 𝑥 }
9 7 8 elrab2 ( 𝐹 ∈ Cauchy ↔ ( 𝐹 ∈ ( ℋ ↑m ℕ ) ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥 ) )
10 ax-hilex ℋ ∈ V
11 nnex ℕ ∈ V
12 10 11 elmap ( 𝐹 ∈ ( ℋ ↑m ℕ ) ↔ 𝐹 : ℕ ⟶ ℋ )
13 12 anbi1i ( ( 𝐹 ∈ ( ℋ ↑m ℕ ) ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥 ) ↔ ( 𝐹 : ℕ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥 ) )
14 9 13 bitri ( 𝐹 ∈ Cauchy ↔ ( 𝐹 : ℕ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥 ) )