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

Metamath Proof Explorer

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 + 𝐻 ) )