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 ) )