Theorem ldualneg

Description: The negative of a scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015)

	Ref	Expression
Hypotheses	ldualneg.r	|- R = ( Scalar ` W )
	ldualneg.m	|- M = ( invg ` R )
	ldualneg.d	|- D = ( LDual ` W )
	ldualneg.s	|- S = ( Scalar ` D )
	ldualneg.n	|- N = ( invg ` S )
	ldualneg.w	|- ( ph -> W e. LMod )
Assertion	ldualneg	|- ( ph -> N = M )

Proof

Step	Hyp	Ref	Expression
1		ldualneg.r	|- R = ( Scalar ` W )
2		ldualneg.m	|- M = ( invg ` R )
3		ldualneg.d	|- D = ( LDual ` W )
4		ldualneg.s	|- S = ( Scalar ` D )
5		ldualneg.n	|- N = ( invg ` S )
6		ldualneg.w	|- ( ph -> W e. LMod )
7		eqid	|- ( oppR ` R ) = ( oppR ` R )
8	1 7 3 4 6	ldualsca	|- ( ph -> S = ( oppR ` R ) )
9	8	fveq2d	|- ( ph -> ( invg ` S ) = ( invg ` ( oppR ` R ) ) )
10	7 2	opprneg	|- M = ( invg ` ( oppR ` R ) )
11	9 5 10	3eqtr4g	|- ( ph -> N = M )