Theorem hdmapln1

Description: Linearity property that will be used for inner product. TODO: try to combine hypotheses in hdmap*ln* series. (Contributed by NM, 7-Jun-2015)

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

Proof

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