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

Metamath Proof Explorer

Theorem hlmet

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

Ref Expression
Hypotheses hlcmet.x ⊢ X = BaseSet ⁡ U
hlcmet.8 ⊢ D = IndMet ⁡ U
Assertion hlmet ⊢ U ∈ CHil OLD → D ∈ Met ⁡ X

Proof

Step Hyp Ref Expression
1 hlcmet.x ⊢ X = BaseSet ⁡ U
2 hlcmet.8 ⊢ D = IndMet ⁡ U
3 1 2 hlcmet ⊢ U ∈ CHil OLD → D ∈ CMet ⁡ X
4 cmetmet ⊢ D ∈ CMet ⁡ X → D ∈ Met ⁡ X
5 3 4 syl ⊢ U ∈ CHil OLD → D ∈ Met ⁡ X