Theorem lflvsdi2a

Description: Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 21-Oct-2014)

	Ref	Expression
Hypotheses	lfldi.v	|- V = ( Base ` W )
	lfldi.r	|- R = ( Scalar ` W )
	lfldi.k	|- K = ( Base ` R )
	lfldi.p	|- .+ = ( +g ` R )
	lfldi.t	|- .x. = ( .r ` R )
	lfldi.f	|- F = ( LFnl ` W )
	lfldi.w	|- ( ph -> W e. LMod )
	lfldi.x	|- ( ph -> X e. K )
	lfldi2.y	|- ( ph -> Y e. K )
	lfldi2.g	|- ( ph -> G e. F )
Assertion	lflvsdi2a	|- ( ph -> ( G oF .x. ( V X. { ( X .+ Y ) } ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .+ ( G oF .x. ( V X. { Y } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lfldi.v	|- V = ( Base ` W )
2		lfldi.r	|- R = ( Scalar ` W )
3		lfldi.k	|- K = ( Base ` R )
4		lfldi.p	|- .+ = ( +g ` R )
5		lfldi.t	|- .x. = ( .r ` R )
6		lfldi.f	|- F = ( LFnl ` W )
7		lfldi.w	|- ( ph -> W e. LMod )
8		lfldi.x	|- ( ph -> X e. K )
9		lfldi2.y	|- ( ph -> Y e. K )
10		lfldi2.g	|- ( ph -> G e. F )
11	1	fvexi	|- V e. _V
12	11	a1i	|- ( ph -> V e. _V )
13	12 8 9	ofc12	|- ( ph -> ( ( V X. { X } ) oF .+ ( V X. { Y } ) ) = ( V X. { ( X .+ Y ) } ) )
14	13	oveq2d	|- ( ph -> ( G oF .x. ( ( V X. { X } ) oF .+ ( V X. { Y } ) ) ) = ( G oF .x. ( V X. { ( X .+ Y ) } ) ) )
15	1 2 3 4 5 6 7 8 9 10	lflvsdi2	|- ( ph -> ( G oF .x. ( ( V X. { X } ) oF .+ ( V X. { Y } ) ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .+ ( G oF .x. ( V X. { Y } ) ) ) )
16	14 15	eqtr3d	|- ( ph -> ( G oF .x. ( V X. { ( X .+ Y ) } ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .+ ( G oF .x. ( V X. { Y } ) ) ) )