Theorem clmvneg1

Description: Minus 1 times a vector is the negative of the vector. Equation 2 of Kreyszig p. 51. ( lmodvneg1 analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	clmvneg1.v	|- V = ( Base ` W )
	clmvneg1.n	|- N = ( invg ` W )
	clmvneg1.f	|- F = ( Scalar ` W )
	clmvneg1.s	|- .x. = ( .s ` W )
Assertion	clmvneg1	|- ( ( W e. CMod /\ X e. V ) -> ( -u 1 .x. X ) = ( N ` X ) )

Proof

Step	Hyp	Ref	Expression
1		clmvneg1.v	|- V = ( Base ` W )
2		clmvneg1.n	|- N = ( invg ` W )
3		clmvneg1.f	|- F = ( Scalar ` W )
4		clmvneg1.s	|- .x. = ( .s ` W )
5		eqid	|- ( Base ` F ) = ( Base ` F )
6	3 5	clmzss	|- ( W e. CMod -> ZZ C_ ( Base ` F ) )
7		1zzd	|- ( W e. CMod -> 1 e. ZZ )
8	6 7	sseldd	|- ( W e. CMod -> 1 e. ( Base ` F ) )
9	3 5	clmneg	|- ( ( W e. CMod /\ 1 e. ( Base ` F ) ) -> -u 1 = ( ( invg ` F ) ` 1 ) )
10	8 9	mpdan	|- ( W e. CMod -> -u 1 = ( ( invg ` F ) ` 1 ) )
11	3	clm1	|- ( W e. CMod -> 1 = ( 1r ` F ) )
12	11	fveq2d	|- ( W e. CMod -> ( ( invg ` F ) ` 1 ) = ( ( invg ` F ) ` ( 1r ` F ) ) )
13	10 12	eqtrd	|- ( W e. CMod -> -u 1 = ( ( invg ` F ) ` ( 1r ` F ) ) )
14	13	adantr	|- ( ( W e. CMod /\ X e. V ) -> -u 1 = ( ( invg ` F ) ` ( 1r ` F ) ) )
15	14	oveq1d	|- ( ( W e. CMod /\ X e. V ) -> ( -u 1 .x. X ) = ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. X ) )
16		clmlmod	|- ( W e. CMod -> W e. LMod )
17		eqid	|- ( 1r ` F ) = ( 1r ` F )
18		eqid	|- ( invg ` F ) = ( invg ` F )
19	1 2 3 4 17 18	lmodvneg1	|- ( ( W e. LMod /\ X e. V ) -> ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. X ) = ( N ` X ) )
20	16 19	sylan	|- ( ( W e. CMod /\ X e. V ) -> ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. X ) = ( N ` X ) )
21	15 20	eqtrd	|- ( ( W e. CMod /\ X e. V ) -> ( -u 1 .x. X ) = ( N ` X ) )