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

Metamath Proof Explorer

Theorem ldualvaddcl

Description: The value of vector addition in the dual of a vector space is a functional. (Contributed by NM, 21-Oct-2014)

Ref Expression
Hypotheses ldualvaddcl.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
ldualvaddcl.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
ldualvaddcl.p ⊢ + = ( +g ‘ 𝐷 )
ldualvaddcl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
ldualvaddcl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
ldualvaddcl.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
Assertion ldualvaddcl ( 𝜑 → ( 𝐺 + 𝐻 ) ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 ldualvaddcl.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2 ldualvaddcl.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
3 ldualvaddcl.p ⊢ + = ( +g ‘ 𝐷 )
4 ldualvaddcl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 ldualvaddcl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
6 ldualvaddcl.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
7 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
8 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
9 1 7 8 2 3 4 5 6 ldualvadd ⊢ ( 𝜑 → ( 𝐺 + 𝐻 ) = ( 𝐺 ∘f ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝐻 ) )
10 7 8 1 4 5 6 lfladdcl ⊢ ( 𝜑 → ( 𝐺 ∘f ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝐻 ) ∈ 𝐹 )
11 9 10 eqeltrd ⊢ ( 𝜑 → ( 𝐺 + 𝐻 ) ∈ 𝐹 )