Metamath Proof Explorer


Theorem nv2

Description: A vector plus itself is two times the vector. (Contributed by NM, 9-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvdi.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
nvdi.2 โŠข ๐บ = ( +๐‘ฃ โ€˜ ๐‘ˆ )
nvdi.4 โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
Assertion nv2 ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐บ ๐ด ) = ( 2 ๐‘† ๐ด ) )

Proof

Step Hyp Ref Expression
1 nvdi.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
2 nvdi.2 โŠข ๐บ = ( +๐‘ฃ โ€˜ ๐‘ˆ )
3 nvdi.4 โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
4 eqid โŠข ( 1st โ€˜ ๐‘ˆ ) = ( 1st โ€˜ ๐‘ˆ )
5 4 nvvc โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ( 1st โ€˜ ๐‘ˆ ) โˆˆ CVecOLD )
6 2 vafval โŠข ๐บ = ( 1st โ€˜ ( 1st โ€˜ ๐‘ˆ ) )
7 3 smfval โŠข ๐‘† = ( 2nd โ€˜ ( 1st โ€˜ ๐‘ˆ ) )
8 1 2 bafval โŠข ๐‘‹ = ran ๐บ
9 6 7 8 vc2OLD โŠข ( ( ( 1st โ€˜ ๐‘ˆ ) โˆˆ CVecOLD โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐บ ๐ด ) = ( 2 ๐‘† ๐ด ) )
10 5 9 sylan โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐บ ๐ด ) = ( 2 ๐‘† ๐ด ) )