Theorem hilcompl

Description: Lemma used for derivation of the completeness axiom ax-hcompl from ZFC Hilbert space theory. The first five hypotheses would be satisfied by the definitions described in ax-hilex ; the 6th would be satisfied by eqid ; the 7th by a given fixed Hilbert space; and the last by Theorem hlcompl . (Contributed by NM, 13-Sep-2007) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hilcompl.1	⊢ ℋ = ( BaseSet ‘ 𝑈 )
	hilcompl.2	⊢ +ℎ = ( +𝑣 ‘ 𝑈 )
	hilcompl.3	⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )
	hilcompl.4	⊢ ·ih = ( ·𝑖OLD ‘ 𝑈 )
	hilcompl.5	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
	hilcompl.6	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	hilcompl.7	⊢ 𝑈 ∈ CHilOLD
	hilcompl.8	⊢ ( 𝐹 ∈ ( Cau ‘ 𝐷 ) → ∃ 𝑥 ∈ ℋ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 )
Assertion	hilcompl	⊢ ( 𝐹 ∈ Cauchy → ∃ 𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		hilcompl.1	⊢ ℋ = ( BaseSet ‘ 𝑈 )
2		hilcompl.2	⊢ +ℎ = ( +𝑣 ‘ 𝑈 )
3		hilcompl.3	⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )
4		hilcompl.4	⊢ ·ih = ( ·𝑖OLD ‘ 𝑈 )
5		hilcompl.5	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
6		hilcompl.6	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
7		hilcompl.7	⊢ 𝑈 ∈ CHilOLD
8		hilcompl.8	⊢ ( 𝐹 ∈ ( Cau ‘ 𝐷 ) → ∃ 𝑥 ∈ ℋ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 )
9	7	hlnvi	⊢ 𝑈 ∈ NrmCVec
10	1 2 3 4 9	hilhhi	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
11	10 5 6 8	hhcmpl	⊢ ( 𝐹 ∈ Cauchy → ∃ 𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥 )