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

Metamath Proof Explorer

Theorem hhssmet

Description: Induced metric of a subspace. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhssims2.1 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
hhssims2.3 ⊢ D = IndMet ⁡ W
hhssims2.2 ⊢ H ∈ S ℋ
Assertion hhssmet ⊢ D ∈ Met ⁡ H

Proof

Step Hyp Ref Expression
1 hhssims2.1 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
2 hhssims2.3 ⊢ D = IndMet ⁡ W
3 hhssims2.2 ⊢ H ∈ S ℋ
4 1 3 hhssnv ⊢ W ∈ NrmCVec
5 1 3 hhssba ⊢ H = BaseSet ⁡ W
6 5 2 imsmet ⊢ W ∈ NrmCVec → D ∈ Met ⁡ H
7 4 6 ax-mp ⊢ D ∈ Met ⁡ H