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

Metamath Proof Explorer

Theorem ldualvaddcom

Description: Commutative law for vector (functional) addition. (Contributed by NM, 17-Jan-2015)

Ref Expression
Hypotheses ldualvaddcom.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
ldualvaddcom.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
ldualvaddcom.p ⊢ + = ( +g ‘ 𝐷 )
ldualvaddcom.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
ldualvaddcom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐹 )
ldualvaddcom.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐹 )
Assertion ldualvaddcom ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ldualvaddcom.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2 ldualvaddcom.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
3 ldualvaddcom.p ⊢ + = ( +g ‘ 𝐷 )
4 ldualvaddcom.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 ldualvaddcom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐹 )
6 ldualvaddcom.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐹 )
7 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
8 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
9 7 8 1 4 5 6 lfladdcom ⊢ ( 𝜑 → ( 𝑋 ∘f ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑌 ) = ( 𝑌 ∘f ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑋 ) )
10 1 7 8 2 3 4 5 6 ldualvadd ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑋 ∘f ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑌 ) )
11 1 7 8 2 3 4 6 5 ldualvadd ⊢ ( 𝜑 → ( 𝑌 + 𝑋 ) = ( 𝑌 ∘f ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑋 ) )
12 9 10 11 3eqtr4d ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )