Theorem clmvz

Description: Two ways to express the negative of a vector. (Contributed by NM, 29-Feb-2008) (Revised by AV, 7-Oct-2021)

	Ref	Expression
Hypotheses	clmvz.v	|- V = ( Base ` W )
	clmvz.m	|- .- = ( -g ` W )
	clmvz.s	|- .x. = ( .s ` W )
	clmvz.0	|- .0. = ( 0g ` W )
Assertion	clmvz	|- ( ( W e. CMod /\ A e. V ) -> ( .0. .- A ) = ( -u 1 .x. A ) )

Proof

Step	Hyp	Ref	Expression
1		clmvz.v	|- V = ( Base ` W )
2		clmvz.m	|- .- = ( -g ` W )
3		clmvz.s	|- .x. = ( .s ` W )
4		clmvz.0	|- .0. = ( 0g ` W )
5		simpl	|- ( ( W e. CMod /\ A e. V ) -> W e. CMod )
6		clmgrp	|- ( W e. CMod -> W e. Grp )
7	1 4	grpidcl	|- ( W e. Grp -> .0. e. V )
8	6 7	syl	|- ( W e. CMod -> .0. e. V )
9	8	adantr	|- ( ( W e. CMod /\ A e. V ) -> .0. e. V )
10		simpr	|- ( ( W e. CMod /\ A e. V ) -> A e. V )
11		eqid	|- ( +g ` W ) = ( +g ` W )
12		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
13	1 11 2 12 3	clmvsubval2	|- ( ( W e. CMod /\ .0. e. V /\ A e. V ) -> ( .0. .- A ) = ( ( -u 1 .x. A ) ( +g ` W ) .0. ) )
14	5 9 10 13	syl3anc	|- ( ( W e. CMod /\ A e. V ) -> ( .0. .- A ) = ( ( -u 1 .x. A ) ( +g ` W ) .0. ) )
15		eqid	|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
16	12 15	clmneg1	|- ( W e. CMod -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
17	16	adantr	|- ( ( W e. CMod /\ A e. V ) -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
18	1 12 3 15	clmvscl	|- ( ( W e. CMod /\ -u 1 e. ( Base ` ( Scalar ` W ) ) /\ A e. V ) -> ( -u 1 .x. A ) e. V )
19	5 17 10 18	syl3anc	|- ( ( W e. CMod /\ A e. V ) -> ( -u 1 .x. A ) e. V )
20	1 11 4	grprid	|- ( ( W e. Grp /\ ( -u 1 .x. A ) e. V ) -> ( ( -u 1 .x. A ) ( +g ` W ) .0. ) = ( -u 1 .x. A ) )
21	6 19 20	syl2an2r	|- ( ( W e. CMod /\ A e. V ) -> ( ( -u 1 .x. A ) ( +g ` W ) .0. ) = ( -u 1 .x. A ) )
22	14 21	eqtrd	|- ( ( W e. CMod /\ A e. V ) -> ( .0. .- A ) = ( -u 1 .x. A ) )