Metamath Proof Explorer


Theorem hhssims2

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 hhssims2 D=norm-H×H

Proof

Step Hyp Ref Expression
1 hhssims2.1 W=+H×H×HnormH
2 hhssims2.3 D=IndMetW
3 hhssims2.2 HS
4 eqid norm-H×H=norm-H×H
5 1 3 4 hhssims norm-H×H=IndMetW
6 2 5 eqtr4i D=norm-H×H