ldualvadd

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

Step	Hyp	Ref	Expression
1		ldualvadd.f	$⊢ F = LFnl (W)$
2		ldualvadd.r	$⊢ R = Scalar (W)$
3		ldualvadd.a	$⊢ \underset{˙}{+} = +_{R}$
4		ldualvadd.d	$⊢ D = LDual (W)$
5		ldualvadd.p	$⊢ \underset{˙}{✚} = +_{D}$
6		ldualvadd.w	$⊢ φ \to W \in X$
7		ldualvadd.g	$⊢ φ \to G \in F$
8		ldualvadd.h	$⊢ φ \to H \in F$
9		eqid	$⊢ {\circ_{f} \underset{˙}{+} ↾}_{(F \times F)} = {\circ_{f} \underset{˙}{+} ↾}_{(F \times F)}$
10	1 2 3 4 5 6 9	ldualfvadd	$⊢ φ \to \underset{˙}{✚} = {\circ_{f} \underset{˙}{+} ↾}_{(F \times F)}$
11	10	oveqd	$⊢ φ \to G \underset{˙}{✚} H = G ({\circ_{f} \underset{˙}{+} ↾}_{(F \times F)}) H$
12	7 8	ofmresval	$⊢ φ \to G ({\circ_{f} \underset{˙}{+} ↾}_{(F \times F)}) H = G {\underset{˙}{+}}_{f} H$
13	11 12	eqtrd	$⊢ φ \to G \underset{˙}{✚} H = G {\underset{˙}{+}}_{f} H$

Metamath Proof Explorer