ldualvaddcl

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

Step	Hyp	Ref	Expression
1		ldualvaddcl.f	$⊢ F = LFnl (W)$
2		ldualvaddcl.d	$⊢ D = LDual (W)$
3		ldualvaddcl.p	$⊢ \underset{˙}{+} = +_{D}$
4		ldualvaddcl.w	$⊢ φ \to W \in LMod$
5		ldualvaddcl.g	$⊢ φ \to G \in F$
6		ldualvaddcl.h	$⊢ φ \to H \in F$
7		eqid	$⊢ Scalar (W) = Scalar (W)$
8		eqid	$⊢ +_{Scalar (W)} = +_{Scalar (W)}$
9	1 7 8 2 3 4 5 6	ldualvadd	$⊢ φ \to G \underset{˙}{+} H = G {+_{Scalar (W)}}_{f} H$
10	7 8 1 4 5 6	lfladdcl	$⊢ φ \to G {+_{Scalar (W)}}_{f} H \in F$
11	9 10	eqeltrd	$⊢ φ \to G \underset{˙}{+} H \in F$

Metamath Proof Explorer