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	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )