Metamath Proof Explorer


Theorem clmvsrinv

Description: A vector minus itself. (Contributed by NM, 4-Dec-2006) (Revised by AV, 28-Sep-2021)

Ref Expression
Hypotheses clmpm1dir.v V=BaseW
clmpm1dir.s ·˙=W
clmpm1dir.a +˙=+W
clmvsrinv.0 0˙=0W
Assertion clmvsrinv WCModAVA+˙-1·˙A=0˙

Proof

Step Hyp Ref Expression
1 clmpm1dir.v V=BaseW
2 clmpm1dir.s ·˙=W
3 clmpm1dir.a +˙=+W
4 clmvsrinv.0 0˙=0W
5 eqid invgW=invgW
6 eqid ScalarW=ScalarW
7 1 5 6 2 clmvneg1 WCModAV-1·˙A=invgWA
8 7 oveq2d WCModAVA+˙-1·˙A=A+˙invgWA
9 clmgrp WCModWGrp
10 1 3 4 5 grprinv WGrpAVA+˙invgWA=0˙
11 9 10 sylan WCModAVA+˙invgWA=0˙
12 8 11 eqtrd WCModAVA+˙-1·˙A=0˙