Metamath Proof Explorer


Theorem nvnegneg

Description: Double negative of a vector. (Contributed by NM, 4-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvnegneg.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
nvnegneg.4 โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
Assertion nvnegneg ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( - 1 ๐‘† ( - 1 ๐‘† ๐ด ) ) = ๐ด )

Proof

Step Hyp Ref Expression
1 nvnegneg.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
2 nvnegneg.4 โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
3 neg1cn โŠข - 1 โˆˆ โ„‚
4 1 2 nvscl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง - 1 โˆˆ โ„‚ โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( - 1 ๐‘† ๐ด ) โˆˆ ๐‘‹ )
5 3 4 mp3an2 โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( - 1 ๐‘† ๐ด ) โˆˆ ๐‘‹ )
6 eqid โŠข ( +๐‘ฃ โ€˜ ๐‘ˆ ) = ( +๐‘ฃ โ€˜ ๐‘ˆ )
7 eqid โŠข ( inv โ€˜ ( +๐‘ฃ โ€˜ ๐‘ˆ ) ) = ( inv โ€˜ ( +๐‘ฃ โ€˜ ๐‘ˆ ) )
8 1 6 2 7 nvinv โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( - 1 ๐‘† ๐ด ) โˆˆ ๐‘‹ ) โ†’ ( - 1 ๐‘† ( - 1 ๐‘† ๐ด ) ) = ( ( inv โ€˜ ( +๐‘ฃ โ€˜ ๐‘ˆ ) ) โ€˜ ( - 1 ๐‘† ๐ด ) ) )
9 5 8 syldan โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( - 1 ๐‘† ( - 1 ๐‘† ๐ด ) ) = ( ( inv โ€˜ ( +๐‘ฃ โ€˜ ๐‘ˆ ) ) โ€˜ ( - 1 ๐‘† ๐ด ) ) )
10 1 6 2 7 nvinv โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( - 1 ๐‘† ๐ด ) = ( ( inv โ€˜ ( +๐‘ฃ โ€˜ ๐‘ˆ ) ) โ€˜ ๐ด ) )
11 10 fveq2d โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( ( inv โ€˜ ( +๐‘ฃ โ€˜ ๐‘ˆ ) ) โ€˜ ( - 1 ๐‘† ๐ด ) ) = ( ( inv โ€˜ ( +๐‘ฃ โ€˜ ๐‘ˆ ) ) โ€˜ ( ( inv โ€˜ ( +๐‘ฃ โ€˜ ๐‘ˆ ) ) โ€˜ ๐ด ) ) )
12 6 nvgrp โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ( +๐‘ฃ โ€˜ ๐‘ˆ ) โˆˆ GrpOp )
13 1 6 bafval โŠข ๐‘‹ = ran ( +๐‘ฃ โ€˜ ๐‘ˆ )
14 13 7 grpo2inv โŠข ( ( ( +๐‘ฃ โ€˜ ๐‘ˆ ) โˆˆ GrpOp โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( ( inv โ€˜ ( +๐‘ฃ โ€˜ ๐‘ˆ ) ) โ€˜ ( ( inv โ€˜ ( +๐‘ฃ โ€˜ ๐‘ˆ ) ) โ€˜ ๐ด ) ) = ๐ด )
15 12 14 sylan โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( ( inv โ€˜ ( +๐‘ฃ โ€˜ ๐‘ˆ ) ) โ€˜ ( ( inv โ€˜ ( +๐‘ฃ โ€˜ ๐‘ˆ ) ) โ€˜ ๐ด ) ) = ๐ด )
16 9 11 15 3eqtrd โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( - 1 ๐‘† ( - 1 ๐‘† ๐ด ) ) = ๐ด )