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

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_ℎ ‘ ( ( 𝐹 ‘ 𝑦 ) −_ℎ ( 𝐹 ‘ 𝑧 ) ) ) < 𝑥 ) )