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

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 )