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=\mathrm{Scalar}\left(W\right)$$
	ldualneg.m	$$⊢M={inv}_g\left(R\right)$$
	ldualneg.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualneg.s	$$⊢S=\mathrm{Scalar}\left(D\right)$$
	ldualneg.n	$$⊢N={inv}_g\left(S\right)$$
	ldualneg.w	$$⊢\phi \to W\in \mathrm{LMod}$$
Assertion	ldualneg	$$⊢\phi \to N=M$$

Proof

Step	Hyp	Ref	Expression
1		ldualneg.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
2		ldualneg.m	$$⊢M={inv}_g\left(R\right)$$
3		ldualneg.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
4		ldualneg.s	$$⊢S=\mathrm{Scalar}\left(D\right)$$
5		ldualneg.n	$$⊢N={inv}_g\left(S\right)$$
6		ldualneg.w	$$⊢\phi \to W\in \mathrm{LMod}$$
7		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
8	1 7 3 4 6	ldualsca	$$⊢\phi \to S={opp}_r\left(R\right)$$
9	8	fveq2d	$$⊢\phi \to {inv}_g\left(S\right)={inv}_g\left({opp}_r\left(R\right)\right)$$
10	7 2	opprneg	$$⊢M={inv}_g\left({opp}_r\left(R\right)\right)$$
11	9 5 10	3eqtr4g	$$⊢\phi \to N=M$$