Metamath Proof Explorer


Theorem sspmval

Description: Vector addition on a subspace in terms of vector addition on the parent space. (Contributed by NM, 28-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses sspm.y
|- Y = ( BaseSet ` W )
sspm.m
|- M = ( -v ` U )
sspm.l
|- L = ( -v ` W )
sspm.h
|- H = ( SubSp ` U )
Assertion sspmval
|- ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A L B ) = ( A M B ) )

Proof

Step Hyp Ref Expression
1 sspm.y
 |-  Y = ( BaseSet ` W )
2 sspm.m
 |-  M = ( -v ` U )
3 sspm.l
 |-  L = ( -v ` W )
4 sspm.h
 |-  H = ( SubSp ` U )
5 4 sspnv
 |-  ( ( U e. NrmCVec /\ W e. H ) -> W e. NrmCVec )
6 neg1cn
 |-  -u 1 e. CC
7 eqid
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
8 1 7 nvscl
 |-  ( ( W e. NrmCVec /\ -u 1 e. CC /\ B e. Y ) -> ( -u 1 ( .sOLD ` W ) B ) e. Y )
9 6 8 mp3an2
 |-  ( ( W e. NrmCVec /\ B e. Y ) -> ( -u 1 ( .sOLD ` W ) B ) e. Y )
10 9 ex
 |-  ( W e. NrmCVec -> ( B e. Y -> ( -u 1 ( .sOLD ` W ) B ) e. Y ) )
11 5 10 syl
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( B e. Y -> ( -u 1 ( .sOLD ` W ) B ) e. Y ) )
12 11 anim2d
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( ( A e. Y /\ B e. Y ) -> ( A e. Y /\ ( -u 1 ( .sOLD ` W ) B ) e. Y ) ) )
13 12 imp
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A e. Y /\ ( -u 1 ( .sOLD ` W ) B ) e. Y ) )
14 eqid
 |-  ( +v ` U ) = ( +v ` U )
15 eqid
 |-  ( +v ` W ) = ( +v ` W )
16 1 14 15 4 sspgval
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ ( -u 1 ( .sOLD ` W ) B ) e. Y ) ) -> ( A ( +v ` W ) ( -u 1 ( .sOLD ` W ) B ) ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` W ) B ) ) )
17 13 16 syldan
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A ( +v ` W ) ( -u 1 ( .sOLD ` W ) B ) ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` W ) B ) ) )
18 eqid
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
19 1 18 7 4 sspsval
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( -u 1 e. CC /\ B e. Y ) ) -> ( -u 1 ( .sOLD ` W ) B ) = ( -u 1 ( .sOLD ` U ) B ) )
20 6 19 mpanr1
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ B e. Y ) -> ( -u 1 ( .sOLD ` W ) B ) = ( -u 1 ( .sOLD ` U ) B ) )
21 20 adantrl
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( -u 1 ( .sOLD ` W ) B ) = ( -u 1 ( .sOLD ` U ) B ) )
22 21 oveq2d
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A ( +v ` U ) ( -u 1 ( .sOLD ` W ) B ) ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) )
23 17 22 eqtrd
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A ( +v ` W ) ( -u 1 ( .sOLD ` W ) B ) ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) )
24 1 15 7 3 nvmval
 |-  ( ( W e. NrmCVec /\ A e. Y /\ B e. Y ) -> ( A L B ) = ( A ( +v ` W ) ( -u 1 ( .sOLD ` W ) B ) ) )
25 24 3expb
 |-  ( ( W e. NrmCVec /\ ( A e. Y /\ B e. Y ) ) -> ( A L B ) = ( A ( +v ` W ) ( -u 1 ( .sOLD ` W ) B ) ) )
26 5 25 sylan
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A L B ) = ( A ( +v ` W ) ( -u 1 ( .sOLD ` W ) B ) ) )
27 eqid
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
28 27 1 4 sspba
 |-  ( ( U e. NrmCVec /\ W e. H ) -> Y C_ ( BaseSet ` U ) )
29 28 sseld
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( A e. Y -> A e. ( BaseSet ` U ) ) )
30 28 sseld
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( B e. Y -> B e. ( BaseSet ` U ) ) )
31 29 30 anim12d
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( ( A e. Y /\ B e. Y ) -> ( A e. ( BaseSet ` U ) /\ B e. ( BaseSet ` U ) ) ) )
32 31 imp
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A e. ( BaseSet ` U ) /\ B e. ( BaseSet ` U ) ) )
33 27 14 18 2 nvmval
 |-  ( ( U e. NrmCVec /\ A e. ( BaseSet ` U ) /\ B e. ( BaseSet ` U ) ) -> ( A M B ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) )
34 33 3expb
 |-  ( ( U e. NrmCVec /\ ( A e. ( BaseSet ` U ) /\ B e. ( BaseSet ` U ) ) ) -> ( A M B ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) )
35 34 adantlr
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. ( BaseSet ` U ) /\ B e. ( BaseSet ` U ) ) ) -> ( A M B ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) )
36 32 35 syldan
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A M B ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) )
37 23 26 36 3eqtr4d
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A L B ) = ( A M B ) )