Theorem hdmapgln2

Description: g-linear property that will be used for inner product. (Contributed by NM, 14-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		hdmapgln2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapgln2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmapgln2.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmapgln2.p	$$⊢\underset{\dot{}}{+}={+}_U$$
5		hdmapgln2.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
6		hdmapgln2.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
7		hdmapgln2.b	$$⊢B={\mathrm{Base}}_R$$
8		hdmapgln2.q	$$⊢\underset{\dot{}}{⨣}={+}_R$$
9		hdmapgln2.m	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
10		hdmapgln2.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
11		hdmapgln2.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
12		hdmapgln2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
13		hdmapgln2.x	$$⊢\phi \to X\in V$$
14		hdmapgln2.y	$$⊢\phi \to Y\in V$$
15		hdmapgln2.z	$$⊢\phi \to Z\in V$$
16		hdmapgln2.a	$$⊢\phi \to A\in B$$
17	1 2 12	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
18	3 6 5 7	lmodvscl	$$⊢\left(U\in \mathrm{LMod}\wedge A\in B\wedge Y\in V\right)\to A\underset{\dot{}}{·}Y\in V$$
19	17 16 14 18	syl3anc	$$⊢\phi \to A\underset{\dot{}}{·}Y\in V$$
20	1 2 3 4 6 8 10 12 13 19 15	hdmaplna2	$$⊢\phi \to S\left(\left(A\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}Z\right)\left(X\right)=S\left(A\underset{\dot{}}{·}Y\right)\left(X\right)\underset{\dot{}}{⨣}S\left(Z\right)\left(X\right)$$
21	1 2 3 5 6 7 9 10 11 12 13 14 16	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)$$
22	21	oveq1d	$$⊢\phi \to S\left(A\underset{\dot{}}{·}Y\right)\left(X\right)\underset{\dot{}}{⨣}S\left(Z\right)\left(X\right)=\left(S\left(Y\right)\left(X\right)\underset{\dot{}}{\times }G\left(A\right)\right)\underset{\dot{}}{⨣}S\left(Z\right)\left(X\right)$$
23	20 22	eqtrd	$$⊢\phi \to S\left(\left(A\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}Z\right)\left(X\right)=\left(S\left(Y\right)\left(X\right)\underset{\dot{}}{\times }G\left(A\right)\right)\underset{\dot{}}{⨣}S\left(Z\right)\left(X\right)$$