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×HnormH
hhssims2.3 D=IndMetW
hhssims2.2 HS
Assertion hhssmet DMetH

Proof

Step Hyp Ref Expression
1 hhssims2.1 W=+H×H×HnormH
2 hhssims2.3 D=IndMetW
3 hhssims2.2 HS
4 1 3 hhssnv WNrmCVec
5 1 3 hhssba H=BaseSetW
6 5 2 imsmet WNrmCVecDMetH
7 4 6 ax-mp DMetH