Theorem ldualvsass

Description: Associative law for scalar product operation. (Contributed by NM, 20-Oct-2014)

	Ref	Expression
Hypotheses	ldualvsass.f	|- F = ( LFnl ` W )
	ldualvsass.r	|- R = ( Scalar ` W )
	ldualvsass.k	|- K = ( Base ` R )
	ldualvsass.t	|- .X. = ( .r ` R )
	ldualvsass.d	|- D = ( LDual ` W )
	ldualvsass.s	|- .x. = ( .s ` D )
	ldualvsass.w	|- ( ph -> W e. LMod )
	ldualvsass.x	|- ( ph -> X e. K )
	ldualvsass.y	|- ( ph -> Y e. K )
	ldualvsass.g	|- ( ph -> G e. F )
Assertion	ldualvsass	|- ( ph -> ( ( Y .X. X ) .x. G ) = ( X .x. ( Y .x. G ) ) )

Proof

Step	Hyp	Ref	Expression
1		ldualvsass.f	|- F = ( LFnl ` W )
2		ldualvsass.r	|- R = ( Scalar ` W )
3		ldualvsass.k	|- K = ( Base ` R )
4		ldualvsass.t	|- .X. = ( .r ` R )
5		ldualvsass.d	|- D = ( LDual ` W )
6		ldualvsass.s	|- .x. = ( .s ` D )
7		ldualvsass.w	|- ( ph -> W e. LMod )
8		ldualvsass.x	|- ( ph -> X e. K )
9		ldualvsass.y	|- ( ph -> Y e. K )
10		ldualvsass.g	|- ( ph -> G e. F )
11		eqid	|- ( Base ` W ) = ( Base ` W )
12	11 2 3 4 1 7 9 8 10	lflvsass	|- ( ph -> ( G oF .X. ( ( Base ` W ) X. { ( Y .X. X ) } ) ) = ( ( G oF .X. ( ( Base ` W ) X. { Y } ) ) oF .X. ( ( Base ` W ) X. { X } ) ) )
13	2	lmodring	|- ( W e. LMod -> R e. Ring )
14	7 13	syl	|- ( ph -> R e. Ring )
15	3 4	ringcl	|- ( ( R e. Ring /\ Y e. K /\ X e. K ) -> ( Y .X. X ) e. K )
16	14 9 8 15	syl3anc	|- ( ph -> ( Y .X. X ) e. K )
17	1 11 2 3 4 5 6 7 16 10	ldualvs	|- ( ph -> ( ( Y .X. X ) .x. G ) = ( G oF .X. ( ( Base ` W ) X. { ( Y .X. X ) } ) ) )
18	11 2 3 4 1 7 10 9	lflvscl	|- ( ph -> ( G oF .X. ( ( Base ` W ) X. { Y } ) ) e. F )
19	1 11 2 3 4 5 6 7 8 18	ldualvs	|- ( ph -> ( X .x. ( G oF .X. ( ( Base ` W ) X. { Y } ) ) ) = ( ( G oF .X. ( ( Base ` W ) X. { Y } ) ) oF .X. ( ( Base ` W ) X. { X } ) ) )
20	12 17 19	3eqtr4d	|- ( ph -> ( ( Y .X. X ) .x. G ) = ( X .x. ( G oF .X. ( ( Base ` W ) X. { Y } ) ) ) )
21	1 11 2 3 4 5 6 7 9 10	ldualvs	|- ( ph -> ( Y .x. G ) = ( G oF .X. ( ( Base ` W ) X. { Y } ) ) )
22	21	oveq2d	|- ( ph -> ( X .x. ( Y .x. G ) ) = ( X .x. ( G oF .X. ( ( Base ` W ) X. { Y } ) ) ) )
23	20 22	eqtr4d	|- ( ph -> ( ( Y .X. X ) .x. G ) = ( X .x. ( Y .x. G ) ) )