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

Metamath Proof Explorer

Theorem ldualvaddval

Description: The value of the value of vector addition in the dual of a vector space. (Contributed by NM, 7-Jan-2015)

Ref Expression
Hypotheses ldualvaddval.v ⊢ V = Base W
ldualvaddval.r ⊢ R = Scalar ⁡ W
ldualvaddval.a ⊢ + ˙ = + R
ldualvaddval.f ⊢ F = LFnl ⁡ W
ldualvaddval.d ⊢ D = LDual ⁡ W
ldualvaddval.p ⊢ ✚ ˙ = + D
ldualvaddval.w ⊢ φ → W ∈ LMod
ldualvaddval.g ⊢ φ → G ∈ F
ldualvaddval.h ⊢ φ → H ∈ F
ldualvaddval.x ⊢ φ → X ∈ V
Assertion ldualvaddval ⊢ φ → G ✚ ˙ H ⁡ X = G ⁡ X + ˙ H ⁡ X

Proof

Step Hyp Ref Expression
1 ldualvaddval.v ⊢ V = Base W
2 ldualvaddval.r ⊢ R = Scalar ⁡ W
3 ldualvaddval.a ⊢ + ˙ = + R
4 ldualvaddval.f ⊢ F = LFnl ⁡ W
5 ldualvaddval.d ⊢ D = LDual ⁡ W
6 ldualvaddval.p ⊢ ✚ ˙ = + D
7 ldualvaddval.w ⊢ φ → W ∈ LMod
8 ldualvaddval.g ⊢ φ → G ∈ F
9 ldualvaddval.h ⊢ φ → H ∈ F
10 ldualvaddval.x ⊢ φ → X ∈ V
11 4 2 3 5 6 7 8 9 ldualvadd ⊢ φ → G ✚ ˙ H = G + ˙ f H
12 11 fveq1d ⊢ φ → G ✚ ˙ H ⁡ X = G + ˙ f H ⁡ X
13 eqid ⊢ Base R = Base R
14 2 13 1 4 lflf ⊢ W ∈ LMod ∧ G ∈ F → G : V ⟶ Base R
15 14 ffnd ⊢ W ∈ LMod ∧ G ∈ F → G Fn V
16 7 8 15 syl2anc ⊢ φ → G Fn V
17 2 13 1 4 lflf ⊢ W ∈ LMod ∧ H ∈ F → H : V ⟶ Base R
18 17 ffnd ⊢ W ∈ LMod ∧ H ∈ F → H Fn V
19 7 9 18 syl2anc ⊢ φ → H Fn V
20 1 fvexi ⊢ V ∈ V
21 20 a1i ⊢ φ → V ∈ V
22 inidm ⊢ V ∩ V = V
23 eqidd ⊢ φ ∧ X ∈ V → G ⁡ X = G ⁡ X
24 eqidd ⊢ φ ∧ X ∈ V → H ⁡ X = H ⁡ X
25 16 19 21 21 22 23 24 ofval ⊢ φ ∧ X ∈ V → G + ˙ f H ⁡ X = G ⁡ X + ˙ H ⁡ X
26 10 25 mpdan ⊢ φ → G + ˙ f H ⁡ X = G ⁡ X + ˙ H ⁡ X
27 12 26 eqtrd ⊢ φ → G ✚ ˙ H ⁡ X = G ⁡ X + ˙ H ⁡ X