Theorem lflvsdi2

Description: Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 19-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	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 } ) ) ) )

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	2 3 1 6	lflf	|- ( ( W e. LMod /\ G e. F ) -> G : V --> K )
14	7 10 13	syl2anc	|- ( ph -> G : V --> K )
15		fconst6g	|- ( X e. K -> ( V X. { X } ) : V --> K )
16	8 15	syl	|- ( ph -> ( V X. { X } ) : V --> K )
17		fconst6g	|- ( Y e. K -> ( V X. { Y } ) : V --> K )
18	9 17	syl	|- ( ph -> ( V X. { Y } ) : V --> K )
19	2	lmodring	|- ( W e. LMod -> R e. Ring )
20	7 19	syl	|- ( ph -> R e. Ring )
21	3 4 5	ringdi	|- ( ( R e. Ring /\ ( x e. K /\ y e. K /\ z e. K ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
22	20 21	sylan	|- ( ( ph /\ ( x e. K /\ y e. K /\ z e. K ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
23	12 14 16 18 22	caofdi	|- ( ph -> ( G oF .x. ( ( V X. { X } ) oF .+ ( V X. { Y } ) ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .+ ( G oF .x. ( V X. { Y } ) ) ) )