Description: A vector minus itself. (Contributed by NM, 4-Dec-2006) (Revised by AV, 28-Sep-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | clmpm1dir.v | |
|
clmpm1dir.s | |
||
clmpm1dir.a | |
||
clmvsrinv.0 | |
||
Assertion | clmvsrinv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clmpm1dir.v | |
|
2 | clmpm1dir.s | |
|
3 | clmpm1dir.a | |
|
4 | clmvsrinv.0 | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | 1 5 6 2 | clmvneg1 | |
8 | 7 | oveq2d | |
9 | clmgrp | |
|
10 | 1 3 4 5 | grprinv | |
11 | 9 10 | sylan | |
12 | 8 11 | eqtrd | |