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 = ( Base ` W )
	clmpm1dir.s	|- .x. = ( .s ` W )
	clmpm1dir.a	|- .+ = ( +g ` W )
	clmvsrinv.0	|- .0. = ( 0g ` W )
Assertion	clmvsrinv	|- ( ( W e. CMod /\ A e. V ) -> ( A .+ ( -u 1 .x. A ) ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		clmpm1dir.v	|- V = ( Base ` W )
2		clmpm1dir.s	|- .x. = ( .s ` W )
3		clmpm1dir.a	|- .+ = ( +g ` W )
4		clmvsrinv.0	|- .0. = ( 0g ` W )
5		eqid	|- ( invg ` W ) = ( invg ` W )
6		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
7	1 5 6 2	clmvneg1	|- ( ( W e. CMod /\ A e. V ) -> ( -u 1 .x. A ) = ( ( invg ` W ) ` A ) )
8	7	oveq2d	|- ( ( W e. CMod /\ A e. V ) -> ( A .+ ( -u 1 .x. A ) ) = ( A .+ ( ( invg ` W ) ` A ) ) )
9		clmgrp	|- ( W e. CMod -> W e. Grp )
10	1 3 4 5	grprinv	|- ( ( W e. Grp /\ A e. V ) -> ( A .+ ( ( invg ` W ) ` A ) ) = .0. )
11	9 10	sylan	|- ( ( W e. CMod /\ A e. V ) -> ( A .+ ( ( invg ` W ) ` A ) ) = .0. )
12	8 11	eqtrd	|- ( ( W e. CMod /\ A e. V ) -> ( A .+ ( -u 1 .x. A ) ) = .0. )