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

Metamath Proof Explorer

Theorem hlcmet

Description: The induced metric on a complex Hilbert space is complete. (Contributed by NM, 8-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses hlcmet.x ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
hlcmet.8 ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
Assertion hlcmet ( 𝑈 ∈ CHilOLD → 𝐷 ∈ ( CMet ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 hlcmet.x ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 hlcmet.8 ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
3 hlobn ⊢ ( 𝑈 ∈ CHilOLD → 𝑈 ∈ CBan )
4 1 2 cbncms ⊢ ( 𝑈 ∈ CBan → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
5 3 4 syl ⊢ ( 𝑈 ∈ CHilOLD → 𝐷 ∈ ( CMet ‘ 𝑋 ) )