Theorem hdmaplna1

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

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

Proof

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