Theorem ldualvadd

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

	Ref	Expression
Hypotheses	ldualvadd.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	ldualvadd.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	ldualvadd.a	⊢ + = ( +g ‘ 𝑅 )
	ldualvadd.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	ldualvadd.p	⊢ ✚ = ( +g ‘ 𝐷 )
	ldualvadd.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
	ldualvadd.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	ldualvadd.h	⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
Assertion	ldualvadd	⊢ ( 𝜑 → ( 𝐺 ✚ 𝐻 ) = ( 𝐺 ∘f + 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		ldualvadd.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2		ldualvadd.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3		ldualvadd.a	⊢ + = ( +g ‘ 𝑅 )
4		ldualvadd.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
5		ldualvadd.p	⊢ ✚ = ( +g ‘ 𝐷 )
6		ldualvadd.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
7		ldualvadd.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
8		ldualvadd.h	⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
9		eqid	⊢ ( ∘f + ↾ ( 𝐹 × 𝐹 ) ) = ( ∘f + ↾ ( 𝐹 × 𝐹 ) )
10	1 2 3 4 5 6 9	ldualfvadd	⊢ ( 𝜑 → ✚ = ( ∘f + ↾ ( 𝐹 × 𝐹 ) ) )
11	10	oveqd	⊢ ( 𝜑 → ( 𝐺 ✚ 𝐻 ) = ( 𝐺 ( ∘f + ↾ ( 𝐹 × 𝐹 ) ) 𝐻 ) )
12	7 8	ofmresval	⊢ ( 𝜑 → ( 𝐺 ( ∘f + ↾ ( 𝐹 × 𝐹 ) ) 𝐻 ) = ( 𝐺 ∘f + 𝐻 ) )
13	11 12	eqtrd	⊢ ( 𝜑 → ( 𝐺 ✚ 𝐻 ) = ( 𝐺 ∘f + 𝐻 ) )