Theorem lmodnegadd

Description: Distribute negation through addition of scalar products. (Contributed by NM, 9-Apr-2015)

	Ref	Expression
Hypotheses	lmodnegadd.v	$$⊢V={\mathrm{Base}}_W$$
	lmodnegadd.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	lmodnegadd.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lmodnegadd.n	$$⊢N={inv}_g\left(W\right)$$
	lmodnegadd.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	lmodnegadd.k	$$⊢K={\mathrm{Base}}_R$$
	lmodnegadd.i	$$⊢I={inv}_g\left(R\right)$$
	lmodnegadd.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lmodnegadd.a	$$⊢\phi \to A\in K$$
	lmodnegadd.b	$$⊢\phi \to B\in K$$
	lmodnegadd.x	$$⊢\phi \to X\in V$$
	lmodnegadd.y	$$⊢\phi \to Y\in V$$
Assertion	lmodnegadd	$$⊢\phi \to N\left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{·}Y\right)\right)=\left(I\left(A\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(I\left(B\right)\underset{\dot{}}{·}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		lmodnegadd.v	$$⊢V={\mathrm{Base}}_W$$
2		lmodnegadd.p	$$⊢\underset{\dot{}}{+}={+}_W$$
3		lmodnegadd.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		lmodnegadd.n	$$⊢N={inv}_g\left(W\right)$$
5		lmodnegadd.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
6		lmodnegadd.k	$$⊢K={\mathrm{Base}}_R$$
7		lmodnegadd.i	$$⊢I={inv}_g\left(R\right)$$
8		lmodnegadd.w	$$⊢\phi \to W\in \mathrm{LMod}$$
9		lmodnegadd.a	$$⊢\phi \to A\in K$$
10		lmodnegadd.b	$$⊢\phi \to B\in K$$
11		lmodnegadd.x	$$⊢\phi \to X\in V$$
12		lmodnegadd.y	$$⊢\phi \to Y\in V$$
13		lmodabl	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$
14	8 13	syl	$$⊢\phi \to W\in \mathrm{Abel}$$
15	1 5 3 6	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge A\in K\wedge X\in V\right)\to A\underset{\dot{}}{·}X\in V$$
16	8 9 11 15	syl3anc	$$⊢\phi \to A\underset{\dot{}}{·}X\in V$$
17	1 5 3 6	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge B\in K\wedge Y\in V\right)\to B\underset{\dot{}}{·}Y\in V$$
18	8 10 12 17	syl3anc	$$⊢\phi \to B\underset{\dot{}}{·}Y\in V$$
19	1 2 4	ablinvadd	$$⊢\left(W\in \mathrm{Abel}\wedge A\underset{\dot{}}{·}X\in V\wedge B\underset{\dot{}}{·}Y\in V\right)\to N\left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{·}Y\right)\right)=N\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}N\left(B\underset{\dot{}}{·}Y\right)$$
20	14 16 18 19	syl3anc	$$⊢\phi \to N\left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{·}Y\right)\right)=N\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}N\left(B\underset{\dot{}}{·}Y\right)$$
21	1 5 3 4 6 7 8 11 9	lmodvsneg	$$⊢\phi \to N\left(A\underset{\dot{}}{·}X\right)=I\left(A\right)\underset{\dot{}}{·}X$$
22	1 5 3 4 6 7 8 12 10	lmodvsneg	$$⊢\phi \to N\left(B\underset{\dot{}}{·}Y\right)=I\left(B\right)\underset{\dot{}}{·}Y$$
23	21 22	oveq12d	$$⊢\phi \to N\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}N\left(B\underset{\dot{}}{·}Y\right)=\left(I\left(A\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(I\left(B\right)\underset{\dot{}}{·}Y\right)$$
24	20 23	eqtrd	$$⊢\phi \to N\left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{·}Y\right)\right)=\left(I\left(A\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(I\left(B\right)\underset{\dot{}}{·}Y\right)$$