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	⊢ 𝑈 = ⟨ ⟨ +_ℎ , ·_ℎ ⟩ , norm_ℎ ⟩
	h2hc.2	⊢ 𝑈 ∈ NrmCVec
	h2hc.3	⊢ ℋ = ( BaseSet ‘ 𝑈 )
	h2hc.4	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
Assertion	h2hcau	⊢ Cauchy = ( ( Cau ‘ 𝐷 ) ∩ ( ℋ ↑_m ℕ ) )

Proof

Step	Hyp	Ref	Expression
1		h2hc.1	⊢ 𝑈 = ⟨ ⟨ +_ℎ , ·_ℎ ⟩ , norm_ℎ ⟩
2		h2hc.2	⊢ 𝑈 ∈ NrmCVec
3		h2hc.3	⊢ ℋ = ( BaseSet ‘ 𝑈 )
4		h2hc.4	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
5		df-rab	⊢ { 𝑓 ∈ ( ℋ ↑_m ℕ ) ∣ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑗 ) −_ℎ ( 𝑓 ‘ 𝑘 ) ) ) < 𝑥 } = { 𝑓 ∣ ( 𝑓 ∈ ( ℋ ↑_m ℕ ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑗 ) −_ℎ ( 𝑓 ‘ 𝑘 ) ) ) < 𝑥 ) }
6		df-hcau	⊢ Cauchy = { 𝑓 ∈ ( ℋ ↑_m ℕ ) ∣ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑗 ) −_ℎ ( 𝑓 ‘ 𝑘 ) ) ) < 𝑥 }
7		elin	⊢ ( 𝑓 ∈ ( ( Cau ‘ 𝐷 ) ∩ ( ℋ ↑_m ℕ ) ) ↔ ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 ∈ ( ℋ ↑_m ℕ ) ) )
8		ancom	⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 ∈ ( ℋ ↑_m ℕ ) ) ↔ ( 𝑓 ∈ ( ℋ ↑_m ℕ ) ∧ 𝑓 ∈ ( Cau ‘ 𝐷 ) ) )
9	3	hlex	⊢ ℋ ∈ V
10		nnex	⊢ ℕ ∈ V
11	9 10	elmap	⊢ ( 𝑓 ∈ ( ℋ ↑_m ℕ ) ↔ 𝑓 : ℕ ⟶ ℋ )
12		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
13	3 4	imsxmet	⊢ ( 𝑈 ∈ NrmCVec → 𝐷 ∈ ( ∞Met ‘ ℋ ) )
14	2 13	mp1i	⊢ ( 𝑓 : ℕ ⟶ ℋ → 𝐷 ∈ ( ∞Met ‘ ℋ ) )
15		1zzd	⊢ ( 𝑓 : ℕ ⟶ ℋ → 1 ∈ ℤ )
16		eqidd	⊢ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) )
17		eqidd	⊢ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑗 ∈ ℕ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑓 ‘ 𝑗 ) )
18		id	⊢ ( 𝑓 : ℕ ⟶ ℋ → 𝑓 : ℕ ⟶ ℋ )
19	12 14 15 16 17 18	iscauf	⊢ ( 𝑓 : ℕ ⟶ ℋ → ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑗 ) 𝐷 ( 𝑓 ‘ 𝑘 ) ) < 𝑥 ) )
20		ffvelcdm	⊢ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑗 ∈ ℕ ) → ( 𝑓 ‘ 𝑗 ) ∈ ℋ )
21	20	adantr	⊢ ( ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( 𝑓 ‘ 𝑗 ) ∈ ℋ )
22		eluznn	⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → 𝑘 ∈ ℕ )
23		ffvelcdm	⊢ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) ∈ ℋ )
24	22 23	sylan2	⊢ ( ( 𝑓 : ℕ ⟶ ℋ ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) ) → ( 𝑓 ‘ 𝑘 ) ∈ ℋ )
25	24	anassrs	⊢ ( ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( 𝑓 ‘ 𝑘 ) ∈ ℋ )
26	1 2 3 4	h2hmetdval	⊢ ( ( ( 𝑓 ‘ 𝑗 ) ∈ ℋ ∧ ( 𝑓 ‘ 𝑘 ) ∈ ℋ ) → ( ( 𝑓 ‘ 𝑗 ) 𝐷 ( 𝑓 ‘ 𝑘 ) ) = ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑗 ) −_ℎ ( 𝑓 ‘ 𝑘 ) ) ) )
27	21 25 26	syl2anc	⊢ ( ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( ( 𝑓 ‘ 𝑗 ) 𝐷 ( 𝑓 ‘ 𝑘 ) ) = ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑗 ) −_ℎ ( 𝑓 ‘ 𝑘 ) ) ) )
28	27	breq1d	⊢ ( ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( ( ( 𝑓 ‘ 𝑗 ) 𝐷 ( 𝑓 ‘ 𝑘 ) ) < 𝑥 ↔ ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑗 ) −_ℎ ( 𝑓 ‘ 𝑘 ) ) ) < 𝑥 ) )
29	28	ralbidva	⊢ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑗 ) 𝐷 ( 𝑓 ‘ 𝑘 ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑗 ) −_ℎ ( 𝑓 ‘ 𝑘 ) ) ) < 𝑥 ) )
30	29	rexbidva	⊢ ( 𝑓 : ℕ ⟶ ℋ → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑗 ) 𝐷 ( 𝑓 ‘ 𝑘 ) ) < 𝑥 ↔ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑗 ) −_ℎ ( 𝑓 ‘ 𝑘 ) ) ) < 𝑥 ) )
31	30	ralbidv	⊢ ( 𝑓 : ℕ ⟶ ℋ → ( ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑗 ) 𝐷 ( 𝑓 ‘ 𝑘 ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑗 ) −_ℎ ( 𝑓 ‘ 𝑘 ) ) ) < 𝑥 ) )
32	19 31	bitrd	⊢ ( 𝑓 : ℕ ⟶ ℋ → ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑗 ) −_ℎ ( 𝑓 ‘ 𝑘 ) ) ) < 𝑥 ) )
33	11 32	sylbi	⊢ ( 𝑓 ∈ ( ℋ ↑_m ℕ ) → ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑗 ) −_ℎ ( 𝑓 ‘ 𝑘 ) ) ) < 𝑥 ) )
34	33	pm5.32i	⊢ ( ( 𝑓 ∈ ( ℋ ↑_m ℕ ) ∧ 𝑓 ∈ ( Cau ‘ 𝐷 ) ) ↔ ( 𝑓 ∈ ( ℋ ↑_m ℕ ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑗 ) −_ℎ ( 𝑓 ‘ 𝑘 ) ) ) < 𝑥 ) )
35	7 8 34	3bitri	⊢ ( 𝑓 ∈ ( ( Cau ‘ 𝐷 ) ∩ ( ℋ ↑_m ℕ ) ) ↔ ( 𝑓 ∈ ( ℋ ↑_m ℕ ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑗 ) −_ℎ ( 𝑓 ‘ 𝑘 ) ) ) < 𝑥 ) )
36	35	eqabi	⊢ ( ( Cau ‘ 𝐷 ) ∩ ( ℋ ↑_m ℕ ) ) = { 𝑓 ∣ ( 𝑓 ∈ ( ℋ ↑_m ℕ ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( norm_ℎ ‘ ( ( 𝑓 ‘ 𝑗 ) −_ℎ ( 𝑓 ‘ 𝑘 ) ) ) < 𝑥 ) }
37	5 6 36	3eqtr4i	⊢ Cauchy = ( ( Cau ‘ 𝐷 ) ∩ ( ℋ ↑_m ℕ ) )

Metamath Proof Explorer

Theorem h2hcau

Proof