Theorem hlim2

Description: The limit of a sequence on a Hilbert space. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	hlim2	⊢ ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐹 ⇝𝑣 𝐴 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑤 = 𝐴 → ( 𝐹 ⇝𝑣 𝑤 ↔ 𝐹 ⇝𝑣 𝐴 ) )
2		oveq2	⊢ ( 𝑤 = 𝐴 → ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝑤 ) = ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) )
3	2	fveq2d	⊢ ( 𝑤 = 𝐴 → ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝑤 ) ) = ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) )
4	3	breq1d	⊢ ( 𝑤 = 𝐴 → ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ↔ ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) )
5	4	rexralbidv	⊢ ( 𝑤 = 𝐴 → ( ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ↔ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) )
6	5	ralbidv	⊢ ( 𝑤 = 𝐴 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) )
7	1 6	bibi12d	⊢ ( 𝑤 = 𝐴 → ( ( 𝐹 ⇝𝑣 𝑤 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ) ↔ ( 𝐹 ⇝𝑣 𝐴 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) ) )
8	7	imbi2d	⊢ ( 𝑤 = 𝐴 → ( ( 𝐹 : ℕ ⟶ ℋ → ( 𝐹 ⇝𝑣 𝑤 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ) ) ↔ ( 𝐹 : ℕ ⟶ ℋ → ( 𝐹 ⇝𝑣 𝐴 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) ) ) )
9		vex	⊢ 𝑤 ∈ V
10	9	hlimi	⊢ ( 𝐹 ⇝𝑣 𝑤 ↔ ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ) )
11	10	baib	⊢ ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝐹 ⇝𝑣 𝑤 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ) )
12	11	expcom	⊢ ( 𝑤 ∈ ℋ → ( 𝐹 : ℕ ⟶ ℋ → ( 𝐹 ⇝𝑣 𝑤 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ) ) )
13	8 12	vtoclga	⊢ ( 𝐴 ∈ ℋ → ( 𝐹 : ℕ ⟶ ℋ → ( 𝐹 ⇝𝑣 𝐴 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) ) )
14	13	impcom	⊢ ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐹 ⇝𝑣 𝐴 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) )