Theorem hdmapglnm2

Description: g-linear property of second (inner product) argument. Line 19 in Holland95 p. 14. (Contributed by NM, 10-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		hdmapglnm2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapglnm2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmapglnm2.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmapglnm2.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
5		hdmapglnm2.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
6		hdmapglnm2.b	$$⊢B={\mathrm{Base}}_R$$
7		hdmapglnm2.m	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
8		hdmapglnm2.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
9		hdmapglnm2.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
10		hdmapglnm2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
11		hdmapglnm2.x	$$⊢\phi \to X\in V$$
12		hdmapglnm2.y	$$⊢\phi \to Y\in V$$
13		hdmapglnm2.z	$$⊢\phi \to A\in B$$
14		eqid	$$⊢\mathrm{LCDual}\left(K\right)\left(W\right)=\mathrm{LCDual}\left(K\right)\left(W\right)$$
15		eqid	$$⊢{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}={\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
16	1 2 3 4 5 6 14 15 8 9 10 12 13	hgmapvs	$$⊢\phi \to S\left(A\underset{\dot{}}{·}Y\right)=G\left(A\right){\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}S\left(Y\right)$$
17	16	fveq1d	$$⊢\phi \to S\left(A\underset{\dot{}}{·}Y\right)\left(X\right)=\left(G\left(A\right){\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}S\left(Y\right)\right)\left(X\right)$$
18		eqid	$$⊢{\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}={\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
19	1 2 5 6 9 10 13	hgmapcl	$$⊢\phi \to G\left(A\right)\in B$$
20	1 2 3 14 18 8 10 12	hdmapcl	$$⊢\phi \to S\left(Y\right)\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
21	1 2 3 5 6 7 14 18 15 10 19 20 11	lcdvsval	$$⊢\phi \to \left(G\left(A\right){\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}S\left(Y\right)\right)\left(X\right)=S\left(Y\right)\left(X\right)\underset{\dot{}}{\times }G\left(A\right)$$
22	17 21	eqtrd	$$⊢\phi \to S\left(A\underset{\dot{}}{·}Y\right)\left(X\right)=S\left(Y\right)\left(X\right)\underset{\dot{}}{\times }G\left(A\right)$$