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