Theorem hdmaplna2

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

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

Proof

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