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

Metamath Proof Explorer

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 ⁡ U
hilcompl.2 ⊢ + ℎ = + v ⁡ U
hilcompl.3 ⊢ ⋅ ℎ = ⋅ 𝑠OLD ⁡ U
hilcompl.4 ⊢ ⋅ ih = ⋅ 𝑖OLD ⁡ U
hilcompl.5 ⊢ D = IndMet ⁡ U
hilcompl.6 ⊢ J = MetOpen ⁡ D
hilcompl.7 ⊢ U ∈ CHil OLD
hilcompl.8 ⊢ F ∈ Cau ⁡ D → ∃ x ∈ ℋ F ⇝t ⁡ J x
Assertion hilcompl ⊢ F ∈ Cauchy → ∃ x ∈ ℋ F ⇝v x

Proof

Step Hyp Ref Expression
1 hilcompl.1 ⊢ ℋ = BaseSet ⁡ U
2 hilcompl.2 ⊢ + ℎ = + v ⁡ U
3 hilcompl.3 ⊢ ⋅ ℎ = ⋅ 𝑠OLD ⁡ U
4 hilcompl.4 ⊢ ⋅ ih = ⋅ 𝑖OLD ⁡ U
5 hilcompl.5 ⊢ D = IndMet ⁡ U
6 hilcompl.6 ⊢ J = MetOpen ⁡ D
7 hilcompl.7 ⊢ U ∈ CHil OLD
8 hilcompl.8 ⊢ F ∈ Cau ⁡ D → ∃ x ∈ ℋ F ⇝t ⁡ J x
9 7 hlnvi ⊢ U ∈ NrmCVec
10 1 2 3 4 9 hilhhi ⊢ U = + ℎ ⋅ ℎ norm ℎ
11 10 5 6 8 hhcmpl ⊢ F ∈ Cauchy → ∃ x ∈ ℋ F ⇝v x