Metamath Proof Explorer


Theorem hhssims

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

Ref Expression
Hypotheses hhsssh2.1 W = + H × H × H norm H
hhssims.2 H S
hhssims.3 D = norm - H × H
Assertion hhssims D = IndMet W

Proof

Step Hyp Ref Expression
1 hhsssh2.1 W = + H × H × H norm H
2 hhssims.2 H S
3 hhssims.3 D = norm - H × H
4 1 2 hhssnv W NrmCVec
5 1 2 hhssvs - H × H = - v W
6 1 hhssnm norm H = norm CV W
7 eqid IndMet W = IndMet W
8 5 6 7 imsval W NrmCVec IndMet W = norm H - H × H
9 4 8 ax-mp IndMet W = norm H - H × H
10 resco norm - H × H = norm - H × H
11 1 2 hhssvsf - H × H : H × H H
12 frn - H × H : H × H H ran - H × H H
13 11 12 ax-mp ran - H × H H
14 cores ran - H × H H norm H - H × H = norm - H × H
15 13 14 ax-mp norm H - H × H = norm - H × H
16 10 15 eqtr4i norm - H × H = norm H - H × H
17 9 16 eqtr4i IndMet W = norm - H × H
18 3 17 eqtr4i D = IndMet W