Theorem hdmaplnm1

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

	Ref	Expression
Hypotheses	hdmaplnm1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmaplnm1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmaplnm1.v	$$⊢V={\mathrm{Base}}_U$$
	hdmaplnm1.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hdmaplnm1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmaplnm1.b	$$⊢B={\mathrm{Base}}_R$$
	hdmaplnm1.m	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
	hdmaplnm1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmaplnm1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmaplnm1.x	$$⊢\phi \to X\in V$$
	hdmaplnm1.y	$$⊢\phi \to Y\in V$$
	hdmaplnm1.a	$$⊢\phi \to A\in B$$
Assertion	hdmaplnm1	$$⊢\phi \to S\left(Y\right)\left(A\underset{\dot{}}{·}X\right)=A\underset{\dot{}}{\times }S\left(Y\right)\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmaplnm1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmaplnm1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmaplnm1.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmaplnm1.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
5		hdmaplnm1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
6		hdmaplnm1.b	$$⊢B={\mathrm{Base}}_R$$
7		hdmaplnm1.m	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
8		hdmaplnm1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
9		hdmaplnm1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		hdmaplnm1.x	$$⊢\phi \to X\in V$$
11		hdmaplnm1.y	$$⊢\phi \to Y\in V$$
12		hdmaplnm1.a	$$⊢\phi \to A\in B$$
13	1 2 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
14		eqid	$$⊢\mathrm{LCDual}\left(K\right)\left(W\right)=\mathrm{LCDual}\left(K\right)\left(W\right)$$
15		eqid	$$⊢{\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}={\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
16		eqid	$$⊢\mathrm{LFnl}\left(U\right)=\mathrm{LFnl}\left(U\right)$$
17	1 2 3 14 15 8 9 11	hdmapcl	$$⊢\phi \to S\left(Y\right)\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
18	1 14 15 2 16 9 17	lcdvbaselfl	$$⊢\phi \to S\left(Y\right)\in \mathrm{LFnl}\left(U\right)$$
19	5 6 7 3 4 16	lflmul	$$⊢\left(U\in \mathrm{LMod}\wedge S\left(Y\right)\in \mathrm{LFnl}\left(U\right)\wedge \left(A\in B\wedge X\in V\right)\right)\to S\left(Y\right)\left(A\underset{\dot{}}{·}X\right)=A\underset{\dot{}}{\times }S\left(Y\right)\left(X\right)$$
20	13 18 12 10 19	syl112anc	$$⊢\phi \to S\left(Y\right)\left(A\underset{\dot{}}{·}X\right)=A\underset{\dot{}}{\times }S\left(Y\right)\left(X\right)$$