This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = inv g ⁡ R
ldualneg.d ⊢ D = LDual ⁡ W
ldualneg.s ⊢ S = Scalar ⁡ D
ldualneg.n ⊢ N = inv g ⁡ S
ldualneg.w ⊢ φ → W ∈ LMod
Assertion ldualneg ⊢ φ → N = M

Proof

Step Hyp Ref Expression
1 ldualneg.r ⊢ R = Scalar ⁡ W
2 ldualneg.m ⊢ M = inv g ⁡ R
3 ldualneg.d ⊢ D = LDual ⁡ W
4 ldualneg.s ⊢ S = Scalar ⁡ D
5 ldualneg.n ⊢ N = inv g ⁡ S
6 ldualneg.w ⊢ φ → W ∈ LMod
7 eqid ⊢ opp r ⁡ R = opp r ⁡ R
8 1 7 3 4 6 ldualsca ⊢ φ → S = opp r ⁡ R
9 8 fveq2d ⊢ φ → inv g ⁡ S = inv g ⁡ opp r ⁡ R
10 7 2 opprneg ⊢ M = inv g ⁡ opp r ⁡ R
11 9 5 10 3eqtr4g ⊢ φ → N = M