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

Metamath Proof Explorer

Theorem ldualsaddN

Description: Scalar addition for the dual of a vector space. (Contributed by NM, 24-Oct-2014) (New usage is discouraged.)

Ref Expression
Hypotheses ldualsadd.f ⊢ F = Scalar ⁡ W
ldualsadd.q ⊢ + ˙ = + F
ldualsadd.d ⊢ D = LDual ⁡ W
ldualsadd.r ⊢ R = Scalar ⁡ D
ldualsadd.p ⊢ ✚ ˙ = + R
ldualsadd.w ⊢ φ → W ∈ V
Assertion ldualsaddN ⊢ φ → ✚ ˙ = + ˙

Proof

Step Hyp Ref Expression
1 ldualsadd.f ⊢ F = Scalar ⁡ W
2 ldualsadd.q ⊢ + ˙ = + F
3 ldualsadd.d ⊢ D = LDual ⁡ W
4 ldualsadd.r ⊢ R = Scalar ⁡ D
5 ldualsadd.p ⊢ ✚ ˙ = + R
6 ldualsadd.w ⊢ φ → W ∈ V
7 eqid ⊢ opp r ⁡ F = opp r ⁡ F
8 1 7 3 4 6 ldualsca ⊢ φ → R = opp r ⁡ F
9 8 fveq2d ⊢ φ → + R = + opp r ⁡ F
10 7 2 oppradd ⊢ + ˙ = + opp r ⁡ F
11 9 5 10 3eqtr4g ⊢ φ → ✚ ˙ = + ˙