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 โŠข ๐‘Œ = ( BaseSet โ€˜ ๐‘Š )
sspm.m โŠข ๐‘€ = ( โˆ’๐‘ฃ โ€˜ ๐‘ˆ )
sspm.l โŠข ๐ฟ = ( โˆ’๐‘ฃ โ€˜ ๐‘Š )
sspm.h โŠข ๐ป = ( SubSp โ€˜ ๐‘ˆ )
Assertion sspmval ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ( ๐ด โˆˆ ๐‘Œ โˆง ๐ต โˆˆ ๐‘Œ ) ) โ†’ ( ๐ด ๐ฟ ๐ต ) = ( ๐ด ๐‘€ ๐ต ) )

Proof

Step Hyp Ref Expression
1 sspm.y โŠข ๐‘Œ = ( BaseSet โ€˜ ๐‘Š )
2 sspm.m โŠข ๐‘€ = ( โˆ’๐‘ฃ โ€˜ ๐‘ˆ )
3 sspm.l โŠข ๐ฟ = ( โˆ’๐‘ฃ โ€˜ ๐‘Š )
4 sspm.h โŠข ๐ป = ( SubSp โ€˜ ๐‘ˆ )
5 4 sspnv โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ๐‘Š โˆˆ NrmCVec )
6 neg1cn โŠข - 1 โˆˆ โ„‚
7 eqid โŠข ( ยท๐‘ OLD โ€˜ ๐‘Š ) = ( ยท๐‘ OLD โ€˜ ๐‘Š )
8 1 7 nvscl โŠข ( ( ๐‘Š โˆˆ NrmCVec โˆง - 1 โˆˆ โ„‚ โˆง ๐ต โˆˆ ๐‘Œ ) โ†’ ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) โˆˆ ๐‘Œ )
9 6 8 mp3an2 โŠข ( ( ๐‘Š โˆˆ NrmCVec โˆง ๐ต โˆˆ ๐‘Œ ) โ†’ ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) โˆˆ ๐‘Œ )
10 9 ex โŠข ( ๐‘Š โˆˆ NrmCVec โ†’ ( ๐ต โˆˆ ๐‘Œ โ†’ ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) โˆˆ ๐‘Œ ) )
11 5 10 syl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ( ๐ต โˆˆ ๐‘Œ โ†’ ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) โˆˆ ๐‘Œ ) )
12 11 anim2d โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ( ( ๐ด โˆˆ ๐‘Œ โˆง ๐ต โˆˆ ๐‘Œ ) โ†’ ( ๐ด โˆˆ ๐‘Œ โˆง ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) โˆˆ ๐‘Œ ) ) )
13 12 imp โŠข ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ( ๐ด โˆˆ ๐‘Œ โˆง ๐ต โˆˆ ๐‘Œ ) ) โ†’ ( ๐ด โˆˆ ๐‘Œ โˆง ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) โˆˆ ๐‘Œ ) )
14 eqid โŠข ( +๐‘ฃ โ€˜ ๐‘ˆ ) = ( +๐‘ฃ โ€˜ ๐‘ˆ )
15 eqid โŠข ( +๐‘ฃ โ€˜ ๐‘Š ) = ( +๐‘ฃ โ€˜ ๐‘Š )
16 1 14 15 4 sspgval โŠข ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ( ๐ด โˆˆ ๐‘Œ โˆง ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) โˆˆ ๐‘Œ ) ) โ†’ ( ๐ด ( +๐‘ฃ โ€˜ ๐‘Š ) ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) ) = ( ๐ด ( +๐‘ฃ โ€˜ ๐‘ˆ ) ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) ) )
17 13 16 syldan โŠข ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ( ๐ด โˆˆ ๐‘Œ โˆง ๐ต โˆˆ ๐‘Œ ) ) โ†’ ( ๐ด ( +๐‘ฃ โ€˜ ๐‘Š ) ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) ) = ( ๐ด ( +๐‘ฃ โ€˜ ๐‘ˆ ) ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) ) )
18 eqid โŠข ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
19 1 18 7 4 sspsval โŠข ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ( - 1 โˆˆ โ„‚ โˆง ๐ต โˆˆ ๐‘Œ ) ) โ†’ ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) = ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐ต ) )
20 6 19 mpanr1 โŠข ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ๐ต โˆˆ ๐‘Œ ) โ†’ ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) = ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐ต ) )
21 20 adantrl โŠข ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ( ๐ด โˆˆ ๐‘Œ โˆง ๐ต โˆˆ ๐‘Œ ) ) โ†’ ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) = ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐ต ) )
22 21 oveq2d โŠข ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ( ๐ด โˆˆ ๐‘Œ โˆง ๐ต โˆˆ ๐‘Œ ) ) โ†’ ( ๐ด ( +๐‘ฃ โ€˜ ๐‘ˆ ) ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) ) = ( ๐ด ( +๐‘ฃ โ€˜ ๐‘ˆ ) ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐ต ) ) )
23 17 22 eqtrd โŠข ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ( ๐ด โˆˆ ๐‘Œ โˆง ๐ต โˆˆ ๐‘Œ ) ) โ†’ ( ๐ด ( +๐‘ฃ โ€˜ ๐‘Š ) ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) ) = ( ๐ด ( +๐‘ฃ โ€˜ ๐‘ˆ ) ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐ต ) ) )
24 1 15 7 3 nvmval โŠข ( ( ๐‘Š โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘Œ โˆง ๐ต โˆˆ ๐‘Œ ) โ†’ ( ๐ด ๐ฟ ๐ต ) = ( ๐ด ( +๐‘ฃ โ€˜ ๐‘Š ) ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) ) )
25 24 3expb โŠข ( ( ๐‘Š โˆˆ NrmCVec โˆง ( ๐ด โˆˆ ๐‘Œ โˆง ๐ต โˆˆ ๐‘Œ ) ) โ†’ ( ๐ด ๐ฟ ๐ต ) = ( ๐ด ( +๐‘ฃ โ€˜ ๐‘Š ) ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) ) )
26 5 25 sylan โŠข ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ( ๐ด โˆˆ ๐‘Œ โˆง ๐ต โˆˆ ๐‘Œ ) ) โ†’ ( ๐ด ๐ฟ ๐ต ) = ( ๐ด ( +๐‘ฃ โ€˜ ๐‘Š ) ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘Š ) ๐ต ) ) )
27 eqid โŠข ( BaseSet โ€˜ ๐‘ˆ ) = ( BaseSet โ€˜ ๐‘ˆ )
28 27 1 4 sspba โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ๐‘Œ โŠ† ( BaseSet โ€˜ ๐‘ˆ ) )
29 28 sseld โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ( ๐ด โˆˆ ๐‘Œ โ†’ ๐ด โˆˆ ( BaseSet โ€˜ ๐‘ˆ ) ) )
30 28 sseld โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ( ๐ต โˆˆ ๐‘Œ โ†’ ๐ต โˆˆ ( BaseSet โ€˜ ๐‘ˆ ) ) )
31 29 30 anim12d โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ( ( ๐ด โˆˆ ๐‘Œ โˆง ๐ต โˆˆ ๐‘Œ ) โ†’ ( ๐ด โˆˆ ( BaseSet โ€˜ ๐‘ˆ ) โˆง ๐ต โˆˆ ( BaseSet โ€˜ ๐‘ˆ ) ) ) )
32 31 imp โŠข ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ( ๐ด โˆˆ ๐‘Œ โˆง ๐ต โˆˆ ๐‘Œ ) ) โ†’ ( ๐ด โˆˆ ( BaseSet โ€˜ ๐‘ˆ ) โˆง ๐ต โˆˆ ( BaseSet โ€˜ ๐‘ˆ ) ) )
33 27 14 18 2 nvmval โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ( BaseSet โ€˜ ๐‘ˆ ) โˆง ๐ต โˆˆ ( BaseSet โ€˜ ๐‘ˆ ) ) โ†’ ( ๐ด ๐‘€ ๐ต ) = ( ๐ด ( +๐‘ฃ โ€˜ ๐‘ˆ ) ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐ต ) ) )
34 33 3expb โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( ๐ด โˆˆ ( BaseSet โ€˜ ๐‘ˆ ) โˆง ๐ต โˆˆ ( BaseSet โ€˜ ๐‘ˆ ) ) ) โ†’ ( ๐ด ๐‘€ ๐ต ) = ( ๐ด ( +๐‘ฃ โ€˜ ๐‘ˆ ) ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐ต ) ) )
35 34 adantlr โŠข ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ( ๐ด โˆˆ ( BaseSet โ€˜ ๐‘ˆ ) โˆง ๐ต โˆˆ ( BaseSet โ€˜ ๐‘ˆ ) ) ) โ†’ ( ๐ด ๐‘€ ๐ต ) = ( ๐ด ( +๐‘ฃ โ€˜ ๐‘ˆ ) ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐ต ) ) )
36 32 35 syldan โŠข ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ( ๐ด โˆˆ ๐‘Œ โˆง ๐ต โˆˆ ๐‘Œ ) ) โ†’ ( ๐ด ๐‘€ ๐ต ) = ( ๐ด ( +๐‘ฃ โ€˜ ๐‘ˆ ) ( - 1 ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐ต ) ) )
37 23 26 36 3eqtr4d โŠข ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ( ๐ด โˆˆ ๐‘Œ โˆง ๐ต โˆˆ ๐‘Œ ) ) โ†’ ( ๐ด ๐ฟ ๐ต ) = ( ๐ด ๐‘€ ๐ต ) )