# 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 X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.`
hhssims.2
`|- H e. SH`
hhssims.3
`|- D = ( ( normh o. -h ) |` ( H X. H ) )`
Assertion hhssims
`|- D = ( IndMet ` W )`

### Proof

Step Hyp Ref Expression
1 hhsssh2.1
` |-  W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.`
2 hhssims.2
` |-  H e. SH`
3 hhssims.3
` |-  D = ( ( normh o. -h ) |` ( H X. H ) )`
4 1 2 hhssnv
` |-  W e. NrmCVec`
5 1 2 hhssvs
` |-  ( -h |` ( H X. H ) ) = ( -v ` W )`
6 1 hhssnm
` |-  ( normh |` H ) = ( normCV ` W )`
7 eqid
` |-  ( IndMet ` W ) = ( IndMet ` W )`
8 5 6 7 imsval
` |-  ( W e. NrmCVec -> ( IndMet ` W ) = ( ( normh |` H ) o. ( -h |` ( H X. H ) ) ) )`
9 4 8 ax-mp
` |-  ( IndMet ` W ) = ( ( normh |` H ) o. ( -h |` ( H X. H ) ) )`
10 resco
` |-  ( ( normh o. -h ) |` ( H X. H ) ) = ( normh o. ( -h |` ( H X. H ) ) )`
11 1 2 hhssvsf
` |-  ( -h |` ( H X. H ) ) : ( H X. H ) --> H`
12 frn
` |-  ( ( -h |` ( H X. H ) ) : ( H X. H ) --> H -> ran ( -h |` ( H X. H ) ) C_ H )`
13 11 12 ax-mp
` |-  ran ( -h |` ( H X. H ) ) C_ H`
14 cores
` |-  ( ran ( -h |` ( H X. H ) ) C_ H -> ( ( normh |` H ) o. ( -h |` ( H X. H ) ) ) = ( normh o. ( -h |` ( H X. H ) ) ) )`
15 13 14 ax-mp
` |-  ( ( normh |` H ) o. ( -h |` ( H X. H ) ) ) = ( normh o. ( -h |` ( H X. H ) ) )`
16 10 15 eqtr4i
` |-  ( ( normh o. -h ) |` ( H X. H ) ) = ( ( normh |` H ) o. ( -h |` ( H X. H ) ) )`
17 9 16 eqtr4i
` |-  ( IndMet ` W ) = ( ( normh o. -h ) |` ( H X. H ) )`
18 3 17 eqtr4i
` |-  D = ( IndMet ` W )`