Theorem hdmaplnm1

Description: Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015)

	Ref	Expression
Hypotheses	hdmaplnm1.h	|- H = ( LHyp ` K )
	hdmaplnm1.u	|- U = ( ( DVecH ` K ) ` W )
	hdmaplnm1.v	|- V = ( Base ` U )
	hdmaplnm1.t	|- .x. = ( .s ` U )
	hdmaplnm1.r	|- R = ( Scalar ` U )
	hdmaplnm1.b	|- B = ( Base ` R )
	hdmaplnm1.m	|- .X. = ( .r ` R )
	hdmaplnm1.s	|- S = ( ( HDMap ` K ) ` W )
	hdmaplnm1.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmaplnm1.x	|- ( ph -> X e. V )
	hdmaplnm1.y	|- ( ph -> Y e. V )
	hdmaplnm1.a	|- ( ph -> A e. B )
Assertion	hdmaplnm1	|- ( ph -> ( ( S ` Y ) ` ( A .x. X ) ) = ( A .X. ( ( S ` Y ) ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmaplnm1.h	|- H = ( LHyp ` K )
2		hdmaplnm1.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmaplnm1.v	|- V = ( Base ` U )
4		hdmaplnm1.t	|- .x. = ( .s ` U )
5		hdmaplnm1.r	|- R = ( Scalar ` U )
6		hdmaplnm1.b	|- B = ( Base ` R )
7		hdmaplnm1.m	|- .X. = ( .r ` R )
8		hdmaplnm1.s	|- S = ( ( HDMap ` K ) ` W )
9		hdmaplnm1.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		hdmaplnm1.x	|- ( ph -> X e. V )
11		hdmaplnm1.y	|- ( ph -> Y e. V )
12		hdmaplnm1.a	|- ( ph -> A e. B )
13	1 2 9	dvhlmod	|- ( ph -> U e. LMod )
14		eqid	|- ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
15		eqid	|- ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
16		eqid	|- ( LFnl ` U ) = ( LFnl ` U )
17	1 2 3 14 15 8 9 11	hdmapcl	|- ( ph -> ( S ` Y ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
18	1 14 15 2 16 9 17	lcdvbaselfl	|- ( ph -> ( S ` Y ) e. ( LFnl ` U ) )
19	5 6 7 3 4 16	lflmul	|- ( ( U e. LMod /\ ( S ` Y ) e. ( LFnl ` U ) /\ ( A e. B /\ X e. V ) ) -> ( ( S ` Y ) ` ( A .x. X ) ) = ( A .X. ( ( S ` Y ) ` X ) ) )
20	13 18 12 10 19	syl112anc	|- ( ph -> ( ( S ` Y ) ` ( A .x. X ) ) = ( A .X. ( ( S ` Y ) ` X ) ) )