Metamath Proof Explorer

Theorem ldualvaddval

Description: The value of the value of vector addition in the dual of a vector space. (Contributed by NM, 7-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 ldualvaddval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 ldualvaddval.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3 ldualvaddval.a ⊢ + = ( +g ‘ 𝑅 )
4 ldualvaddval.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
5 ldualvaddval.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
6 ldualvaddval.p ⊢ ✚ = ( +g ‘ 𝐷 )
7 ldualvaddval.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
8 ldualvaddval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9 ldualvaddval.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
10 ldualvaddval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
11 4 2 3 5 6 7 8 9 ldualvadd ⊢ ( 𝜑 → ( 𝐺 ✚ 𝐻 ) = ( 𝐺 ∘f + 𝐻 ) )
12 11 fveq1d ⊢ ( 𝜑 → ( ( 𝐺 ✚ 𝐻 ) ‘ 𝑋 ) = ( ( 𝐺 ∘f + 𝐻 ) ‘ 𝑋 ) )
13 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14 2 13 1 4 lflf ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝑅 ) )
15 14 ffnd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 Fn 𝑉 )
16 7 8 15 syl2anc ⊢ ( 𝜑 → 𝐺 Fn 𝑉 )
17 2 13 1 4 lflf ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ) → 𝐻 : 𝑉 ⟶ ( Base ‘ 𝑅 ) )
18 17 ffnd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ) → 𝐻 Fn 𝑉 )
19 7 9 18 syl2anc ⊢ ( 𝜑 → 𝐻 Fn 𝑉 )
20 1 fvexi ⊢ 𝑉 ∈ V
21 20 a1i ⊢ ( 𝜑 → 𝑉 ∈ V )
22 inidm ⊢ ( 𝑉 ∩ 𝑉 ) = 𝑉
23 eqidd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )
24 eqidd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑋 ) = ( 𝐻 ‘ 𝑋 ) )
25 16 19 21 21 22 23 24 ofval ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐺 ∘f + 𝐻 ) ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) + ( 𝐻 ‘ 𝑋 ) ) )
26 10 25 mpdan ⊢ ( 𝜑 → ( ( 𝐺 ∘f + 𝐻 ) ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) + ( 𝐻 ‘ 𝑋 ) ) )
27 12 26 eqtrd ⊢ ( 𝜑 → ( ( 𝐺 ✚ 𝐻 ) ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) + ( 𝐻 ‘ 𝑋 ) ) )