Metamath Proof Explorer


Theorem hvsubid

Description: Subtraction of a vector from itself. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

Ref Expression
Assertion hvsubid ( ๐ด โˆˆ โ„‹ โ†’ ( ๐ด โˆ’โ„Ž ๐ด ) = 0โ„Ž )

Proof

Step Hyp Ref Expression
1 ax-hvmulid โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( 1 ยทโ„Ž ๐ด ) = ๐ด )
2 1 oveq1d โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ( 1 ยทโ„Ž ๐ด ) +โ„Ž ( - 1 ยทโ„Ž ๐ด ) ) = ( ๐ด +โ„Ž ( - 1 ยทโ„Ž ๐ด ) ) )
3 ax-1cn โŠข 1 โˆˆ โ„‚
4 neg1cn โŠข - 1 โˆˆ โ„‚
5 ax-hvdistr2 โŠข ( ( 1 โˆˆ โ„‚ โˆง - 1 โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‹ ) โ†’ ( ( 1 + - 1 ) ยทโ„Ž ๐ด ) = ( ( 1 ยทโ„Ž ๐ด ) +โ„Ž ( - 1 ยทโ„Ž ๐ด ) ) )
6 3 4 5 mp3an12 โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ( 1 + - 1 ) ยทโ„Ž ๐ด ) = ( ( 1 ยทโ„Ž ๐ด ) +โ„Ž ( - 1 ยทโ„Ž ๐ด ) ) )
7 hvsubval โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โˆˆ โ„‹ ) โ†’ ( ๐ด โˆ’โ„Ž ๐ด ) = ( ๐ด +โ„Ž ( - 1 ยทโ„Ž ๐ด ) ) )
8 7 anidms โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ๐ด โˆ’โ„Ž ๐ด ) = ( ๐ด +โ„Ž ( - 1 ยทโ„Ž ๐ด ) ) )
9 2 6 8 3eqtr4rd โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ๐ด โˆ’โ„Ž ๐ด ) = ( ( 1 + - 1 ) ยทโ„Ž ๐ด ) )
10 1pneg1e0 โŠข ( 1 + - 1 ) = 0
11 10 oveq1i โŠข ( ( 1 + - 1 ) ยทโ„Ž ๐ด ) = ( 0 ยทโ„Ž ๐ด )
12 9 11 eqtrdi โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ๐ด โˆ’โ„Ž ๐ด ) = ( 0 ยทโ„Ž ๐ด ) )
13 ax-hvmul0 โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( 0 ยทโ„Ž ๐ด ) = 0โ„Ž )
14 12 13 eqtrd โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ๐ด โˆ’โ„Ž ๐ด ) = 0โ„Ž )