Theorem clmvsneg

Description: Multiplication of a vector by a negated scalar. ( lmodvsneg analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	clmvsneg.b	|- B = ( Base ` W )
	clmvsneg.f	|- F = ( Scalar ` W )
	clmvsneg.s	|- .x. = ( .s ` W )
	clmvsneg.n	|- N = ( invg ` W )
	clmvsneg.k	|- K = ( Base ` F )
	clmvsneg.w	|- ( ph -> W e. CMod )
	clmvsneg.x	|- ( ph -> X e. B )
	clmvsneg.r	|- ( ph -> R e. K )
Assertion	clmvsneg	|- ( ph -> ( N ` ( R .x. X ) ) = ( -u R .x. X ) )

Proof

Step	Hyp	Ref	Expression
1		clmvsneg.b	|- B = ( Base ` W )
2		clmvsneg.f	|- F = ( Scalar ` W )
3		clmvsneg.s	|- .x. = ( .s ` W )
4		clmvsneg.n	|- N = ( invg ` W )
5		clmvsneg.k	|- K = ( Base ` F )
6		clmvsneg.w	|- ( ph -> W e. CMod )
7		clmvsneg.x	|- ( ph -> X e. B )
8		clmvsneg.r	|- ( ph -> R e. K )
9		eqid	|- ( invg ` F ) = ( invg ` F )
10		clmlmod	|- ( W e. CMod -> W e. LMod )
11	6 10	syl	|- ( ph -> W e. LMod )
12	1 2 3 4 5 9 11 7 8	lmodvsneg	|- ( ph -> ( N ` ( R .x. X ) ) = ( ( ( invg ` F ) ` R ) .x. X ) )
13	2 5	clmneg	|- ( ( W e. CMod /\ R e. K ) -> -u R = ( ( invg ` F ) ` R ) )
14	6 8 13	syl2anc	|- ( ph -> -u R = ( ( invg ` F ) ` R ) )
15	14	oveq1d	|- ( ph -> ( -u R .x. X ) = ( ( ( invg ` F ) ` R ) .x. X ) )
16	12 15	eqtr4d	|- ( ph -> ( N ` ( R .x. X ) ) = ( -u R .x. X ) )