h2hlm

Description: The limit sequences of Hilbert space. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 13-May-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022) (New usage is discouraged.)

	Ref	Expression
Hypotheses	h2hl.1	⊢ 𝑈 = ⟨ ⟨ +_ℎ , ·_ℎ ⟩ , norm_ℎ ⟩
	h2hl.2	⊢ 𝑈 ∈ NrmCVec
	h2hl.3	⊢ ℋ = ( BaseSet ‘ 𝑈 )
	h2hl.4	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
	h2hl.5	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion	h2hlm	⊢ ⇝_𝑣 = ( ( ⇝_𝑡 ‘ 𝐽 ) ↾ ( ℋ ↑_m ℕ ) )

Proof

Step	Hyp	Ref	Expression
1		h2hl.1	⊢ 𝑈 = ⟨ ⟨ +_ℎ , ·_ℎ ⟩ , norm_ℎ ⟩
2		h2hl.2	⊢ 𝑈 ∈ NrmCVec
3		h2hl.3	⊢ ℋ = ( BaseSet ‘ 𝑈 )
4		h2hl.4	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
5		h2hl.5	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
6		df-hlim	⊢ ⇝_𝑣 = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) }
7	6	relopabiv	⊢ Rel ⇝_𝑣
8		relres	⊢ Rel ( ( ⇝_𝑡 ‘ 𝐽 ) ↾ ( ℋ ↑_m ℕ ) )
9	6	eleq2i	⊢ ( ⟨ 𝑓 , 𝑥 ⟩ ∈ ⇝_𝑣 ↔ ⟨ 𝑓 , 𝑥 ⟩ ∈ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) } )
10		opabidw	⊢ ( ⟨ 𝑓 , 𝑥 ⟩ ∈ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) } ↔ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) )
11	3	hlex	⊢ ℋ ∈ V
12		nnex	⊢ ℕ ∈ V
13	11 12	elmap	⊢ ( 𝑓 ∈ ( ℋ ↑_m ℕ ) ↔ 𝑓 : ℕ ⟶ ℋ )
14	13	anbi1i	⊢ ( ( 𝑓 ∈ ( ℋ ↑_m ℕ ) ∧ ⟨ 𝑓 , 𝑥 ⟩ ∈ ( ⇝_𝑡 ‘ 𝐽 ) ) ↔ ( 𝑓 : ℕ ⟶ ℋ ∧ ⟨ 𝑓 , 𝑥 ⟩ ∈ ( ⇝_𝑡 ‘ 𝐽 ) ) )
15		df-br	⊢ ( 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ↔ ⟨ 𝑓 , 𝑥 ⟩ ∈ ( ⇝_𝑡 ‘ 𝐽 ) )
16	3 4	imsxmet	⊢ ( 𝑈 ∈ NrmCVec → 𝐷 ∈ ( ∞Met ‘ ℋ ) )
17	2 16	mp1i	⊢ ( 𝑓 : ℕ ⟶ ℋ → 𝐷 ∈ ( ∞Met ‘ ℋ ) )
18		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
19		1zzd	⊢ ( 𝑓 : ℕ ⟶ ℋ → 1 ∈ ℤ )
20		eqidd	⊢ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) )
21		id	⊢ ( 𝑓 : ℕ ⟶ ℋ → 𝑓 : ℕ ⟶ ℋ )
22	5 17 18 19 20 21	lmmbrf	⊢ ( 𝑓 : ℕ ⟶ ℋ → ( 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ↔ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) 𝐷 𝑥 ) < 𝑦 ) ) )
23		eluznn	⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → 𝑘 ∈ ℕ )
24		ffvelcdm	⊢ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) ∈ ℋ )
25	1 2 3 4	h2hmetdval	⊢ ( ( ( 𝑓 ‘ 𝑘 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑓 ‘ 𝑘 ) 𝐷 𝑥 ) = ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) )
26	24 25	sylan	⊢ ( ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑓 ‘ 𝑘 ) 𝐷 𝑥 ) = ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) )
27	26	breq1d	⊢ ( ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑓 ‘ 𝑘 ) 𝐷 𝑥 ) < 𝑦 ↔ ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) )
28	27	an32s	⊢ ( ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑓 ‘ 𝑘 ) 𝐷 𝑥 ) < 𝑦 ↔ ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) )
29	23 28	sylan2	⊢ ( ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) ) → ( ( ( 𝑓 ‘ 𝑘 ) 𝐷 𝑥 ) < 𝑦 ↔ ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) )
30	29	anassrs	⊢ ( ( ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( ( ( 𝑓 ‘ 𝑘 ) 𝐷 𝑥 ) < 𝑦 ↔ ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) )
31	30	ralbidva	⊢ ( ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) 𝐷 𝑥 ) < 𝑦 ↔ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) )
32	31	rexbidva	⊢ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) 𝐷 𝑥 ) < 𝑦 ↔ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) )
33	32	ralbidv	⊢ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) 𝐷 𝑥 ) < 𝑦 ↔ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) )
34	33	pm5.32da	⊢ ( 𝑓 : ℕ ⟶ ℋ → ( ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) 𝐷 𝑥 ) < 𝑦 ) ↔ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) ) )
35	22 34	bitrd	⊢ ( 𝑓 : ℕ ⟶ ℋ → ( 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ↔ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) ) )
36	15 35	bitr3id	⊢ ( 𝑓 : ℕ ⟶ ℋ → ( ⟨ 𝑓 , 𝑥 ⟩ ∈ ( ⇝_𝑡 ‘ 𝐽 ) ↔ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) ) )
37	36	pm5.32i	⊢ ( ( 𝑓 : ℕ ⟶ ℋ ∧ ⟨ 𝑓 , 𝑥 ⟩ ∈ ( ⇝_𝑡 ‘ 𝐽 ) ) ↔ ( 𝑓 : ℕ ⟶ ℋ ∧ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) ) )
38	14 37	bitr2i	⊢ ( ( 𝑓 : ℕ ⟶ ℋ ∧ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) ) ↔ ( 𝑓 ∈ ( ℋ ↑_m ℕ ) ∧ ⟨ 𝑓 , 𝑥 ⟩ ∈ ( ⇝_𝑡 ‘ 𝐽 ) ) )
39		anass	⊢ ( ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) ↔ ( 𝑓 : ℕ ⟶ ℋ ∧ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) ) )
40		opelres	⊢ ( 𝑥 ∈ V → ( ⟨ 𝑓 , 𝑥 ⟩ ∈ ( ( ⇝_𝑡 ‘ 𝐽 ) ↾ ( ℋ ↑_m ℕ ) ) ↔ ( 𝑓 ∈ ( ℋ ↑_m ℕ ) ∧ ⟨ 𝑓 , 𝑥 ⟩ ∈ ( ⇝_𝑡 ‘ 𝐽 ) ) ) )
41	40	elv	⊢ ( ⟨ 𝑓 , 𝑥 ⟩ ∈ ( ( ⇝_𝑡 ‘ 𝐽 ) ↾ ( ℋ ↑_m ℕ ) ) ↔ ( 𝑓 ∈ ( ℋ ↑_m ℕ ) ∧ ⟨ 𝑓 , 𝑥 ⟩ ∈ ( ⇝_𝑡 ‘ 𝐽 ) ) )
42	38 39 41	3bitr4i	⊢ ( ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑘 ) −_ℎ 𝑥 ) ) < 𝑦 ) ↔ ⟨ 𝑓 , 𝑥 ⟩ ∈ ( ( ⇝_𝑡 ‘ 𝐽 ) ↾ ( ℋ ↑_m ℕ ) ) )
43	9 10 42	3bitri	⊢ ( ⟨ 𝑓 , 𝑥 ⟩ ∈ ⇝_𝑣 ↔ ⟨ 𝑓 , 𝑥 ⟩ ∈ ( ( ⇝_𝑡 ‘ 𝐽 ) ↾ ( ℋ ↑_m ℕ ) ) )
44	7 8 43	eqrelriiv	⊢ ⇝_𝑣 = ( ( ⇝_𝑡 ‘ 𝐽 ) ↾ ( ℋ ↑_m ℕ ) )

Metamath Proof Explorer

Theorem h2hlm

Proof