Metamath Proof Explorer

Theorem sspimsval

Description: The induced metric on a subspace in terms of the induced metric on the parent space. (Contributed by NM, 1-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses sspims.y 
|- Y = ( BaseSet ` W )
sspims.d 
|- D = ( IndMet ` U )
sspims.c 
|- C = ( IndMet ` W )
sspims.h 
|- H = ( SubSp ` U )
Assertion sspimsval 
|- ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A C B ) = ( A D B ) )

Proof

Step Hyp Ref Expression
1 sspims.y 
 |-  Y = ( BaseSet ` W )
2 sspims.d 
 |-  D = ( IndMet ` U )
3 sspims.c 
 |-  C = ( IndMet ` W )
4 sspims.h 
 |-  H = ( SubSp ` U )
5 4 sspnv 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> W e. NrmCVec )
6 eqid 
 |-  ( -v ` W ) = ( -v ` W )
7 1 6 nvmcl 
 |-  ( ( W e. NrmCVec /\ A e. Y /\ B e. Y ) -> ( A ( -v ` W ) B ) e. Y )
8 7 3expb 
 |-  ( ( W e. NrmCVec /\ ( A e. Y /\ B e. Y ) ) -> ( A ( -v ` W ) B ) e. Y )
9 5 8 sylan 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A ( -v ` W ) B ) e. Y )
10 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
11 eqid 
 |-  ( normCV ` W ) = ( normCV ` W )
12 1 10 11 4 sspnval 
 |-  ( ( U e. NrmCVec /\ W e. H /\ ( A ( -v ` W ) B ) e. Y ) -> ( ( normCV ` W ) ` ( A ( -v ` W ) B ) ) = ( ( normCV ` U ) ` ( A ( -v ` W ) B ) ) )
13 12 3expa 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A ( -v ` W ) B ) e. Y ) -> ( ( normCV ` W ) ` ( A ( -v ` W ) B ) ) = ( ( normCV ` U ) ` ( A ( -v ` W ) B ) ) )
14 9 13 syldan 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( ( normCV ` W ) ` ( A ( -v ` W ) B ) ) = ( ( normCV ` U ) ` ( A ( -v ` W ) B ) ) )
15 eqid 
 |-  ( -v ` U ) = ( -v ` U )
16 1 15 6 4 sspmval 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A ( -v ` W ) B ) = ( A ( -v ` U ) B ) )
17 16 fveq2d 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( ( normCV ` U ) ` ( A ( -v ` W ) B ) ) = ( ( normCV ` U ) ` ( A ( -v ` U ) B ) ) )
18 14 17 eqtrd 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( ( normCV ` W ) ` ( A ( -v ` W ) B ) ) = ( ( normCV ` U ) ` ( A ( -v ` U ) B ) ) )
19 1 6 11 3 imsdval 
 |-  ( ( W e. NrmCVec /\ A e. Y /\ B e. Y ) -> ( A C B ) = ( ( normCV ` W ) ` ( A ( -v ` W ) B ) ) )
20 19 3expb 
 |-  ( ( W e. NrmCVec /\ ( A e. Y /\ B e. Y ) ) -> ( A C B ) = ( ( normCV ` W ) ` ( A ( -v ` W ) B ) ) )
21 5 20 sylan 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A C B ) = ( ( normCV ` W ) ` ( A ( -v ` W ) B ) ) )
22 eqid 
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
23 22 1 4 sspba 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> Y C_ ( BaseSet ` U ) )
24 23 sseld 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( A e. Y -> A e. ( BaseSet ` U ) ) )
25 23 sseld 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( B e. Y -> B e. ( BaseSet ` U ) ) )
26 24 25 anim12d 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( ( A e. Y /\ B e. Y ) -> ( A e. ( BaseSet ` U ) /\ B e. ( BaseSet ` U ) ) ) )
27 26 imp 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A e. ( BaseSet ` U ) /\ B e. ( BaseSet ` U ) ) )
28 22 15 10 2 imsdval 
 |-  ( ( U e. NrmCVec /\ A e. ( BaseSet ` U ) /\ B e. ( BaseSet ` U ) ) -> ( A D B ) = ( ( normCV ` U ) ` ( A ( -v ` U ) B ) ) )
29 28 3expb 
 |-  ( ( U e. NrmCVec /\ ( A e. ( BaseSet ` U ) /\ B e. ( BaseSet ` U ) ) ) -> ( A D B ) = ( ( normCV ` U ) ` ( A ( -v ` U ) B ) ) )
30 29 adantlr 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. ( BaseSet ` U ) /\ B e. ( BaseSet ` U ) ) ) -> ( A D B ) = ( ( normCV ` U ) ` ( A ( -v ` U ) B ) ) )
31 27 30 syldan 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A D B ) = ( ( normCV ` U ) ` ( A ( -v ` U ) B ) ) )
32 18 21 31 3eqtr4d 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A C B ) = ( A D B ) )