Theorem ldualvsass2

Description: Associative law for scalar product operation, using operations from the dual space. (Contributed by NM, 20-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ldualvsass2.f	|- F = ( LFnl ` W )
2		ldualvsass2.r	|- R = ( Scalar ` W )
3		ldualvsass2.k	|- K = ( Base ` R )
4		ldualvsass2.d	|- D = ( LDual ` W )
5		ldualvsass2.q	|- Q = ( Scalar ` D )
6		ldualvsass2.t	|- .X. = ( .r ` Q )
7		ldualvsass2.s	|- .x. = ( .s ` D )
8		ldualvsass2.w	|- ( ph -> W e. LMod )
9		ldualvsass2.x	|- ( ph -> X e. K )
10		ldualvsass2.y	|- ( ph -> Y e. K )
11		ldualvsass2.g	|- ( ph -> G e. F )
12		eqid	|- ( .r ` R ) = ( .r ` R )
13	2 3 12 4 5 6 8 9 10	ldualsmul	|- ( ph -> ( X .X. Y ) = ( Y ( .r ` R ) X ) )
14	13	oveq1d	|- ( ph -> ( ( X .X. Y ) .x. G ) = ( ( Y ( .r ` R ) X ) .x. G ) )
15	1 2 3 12 4 7 8 9 10 11	ldualvsass	|- ( ph -> ( ( Y ( .r ` R ) X ) .x. G ) = ( X .x. ( Y .x. G ) ) )
16	14 15	eqtrd	|- ( ph -> ( ( X .X. Y ) .x. G ) = ( X .x. ( Y .x. G ) ) )