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	⊢ ( 𝜑 → ( 𝐺 + 𝐻 ) ∈ 𝐹 )