Theorem hdmaplns1

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

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

Proof

Step	Hyp	Ref	Expression
1		hdmaplns1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmaplns1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmaplns1.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmaplns1.m	$$⊢\underset{\dot{}}{-}={-}_U$$
5		hdmaplns1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
6		hdmaplns1.n	$$⊢N={-}_R$$
7		hdmaplns1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
8		hdmaplns1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		hdmaplns1.x	$$⊢\phi \to X\in V$$
10		hdmaplns1.y	$$⊢\phi \to Y\in V$$
11		hdmaplns1.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	lflsub	$$⊢\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)NS\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)NS\left(Z\right)\left(Y\right)$$