Theorem ldualvaddcom

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

	Ref	Expression
Hypotheses	ldualvaddcom.f	|- F = ( LFnl ` W )
	ldualvaddcom.d	|- D = ( LDual ` W )
	ldualvaddcom.p	|- .+ = ( +g ` D )
	ldualvaddcom.w	|- ( ph -> W e. LMod )
	ldualvaddcom.x	|- ( ph -> X e. F )
	ldualvaddcom.y	|- ( ph -> Y e. F )
Assertion	ldualvaddcom	|- ( ph -> ( X .+ Y ) = ( Y .+ X ) )

Proof

Step	Hyp	Ref	Expression
1		ldualvaddcom.f	|- F = ( LFnl ` W )
2		ldualvaddcom.d	|- D = ( LDual ` W )
3		ldualvaddcom.p	|- .+ = ( +g ` D )
4		ldualvaddcom.w	|- ( ph -> W e. LMod )
5		ldualvaddcom.x	|- ( ph -> X e. F )
6		ldualvaddcom.y	|- ( ph -> Y e. F )
7		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
8		eqid	|- ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
9	7 8 1 4 5 6	lfladdcom	|- ( ph -> ( X oF ( +g ` ( Scalar ` W ) ) Y ) = ( Y oF ( +g ` ( Scalar ` W ) ) X ) )
10	1 7 8 2 3 4 5 6	ldualvadd	|- ( ph -> ( X .+ Y ) = ( X oF ( +g ` ( Scalar ` W ) ) Y ) )
11	1 7 8 2 3 4 6 5	ldualvadd	|- ( ph -> ( Y .+ X ) = ( Y oF ( +g ` ( Scalar ` W ) ) X ) )
12	9 10 11	3eqtr4d	|- ( ph -> ( X .+ Y ) = ( Y .+ X ) )