Theorem lvecindp2

Description: Sums of independent vectors must have equal coefficients. (Contributed by NM, 22-Mar-2015)

	Ref	Expression
Hypotheses	lvecindp2.v	$$⊢V={\mathrm{Base}}_W$$
	lvecindp2.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	lvecindp2.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lvecindp2.k	$$⊢K={\mathrm{Base}}_F$$
	lvecindp2.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lvecindp2.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lvecindp2.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lvecindp2.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lvecindp2.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lvecindp2.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lvecindp2.a	$$⊢\phi \to A\in K$$
	lvecindp2.b	$$⊢\phi \to B\in K$$
	lvecindp2.c	$$⊢\phi \to C\in K$$
	lvecindp2.d	$$⊢\phi \to D\in K$$
	lvecindp2.q	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
	lvecindp2.e	$$⊢\phi \to \left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{·}Y\right)=\left(C\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(D\underset{\dot{}}{·}Y\right)$$
Assertion	lvecindp2	$$⊢\phi \to \left(A=C\wedge B=D\right)$$

Proof

Step	Hyp	Ref	Expression
1		lvecindp2.v	$$⊢V={\mathrm{Base}}_W$$
2		lvecindp2.p	$$⊢\underset{\dot{}}{+}={+}_W$$
3		lvecindp2.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		lvecindp2.k	$$⊢K={\mathrm{Base}}_F$$
5		lvecindp2.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		lvecindp2.o	$$⊢\underset{\dot{}}{0}=0_W$$
7		lvecindp2.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
8		lvecindp2.w	$$⊢\phi \to W\in \mathrm{LVec}$$
9		lvecindp2.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
10		lvecindp2.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
11		lvecindp2.a	$$⊢\phi \to A\in K$$
12		lvecindp2.b	$$⊢\phi \to B\in K$$
13		lvecindp2.c	$$⊢\phi \to C\in K$$
14		lvecindp2.d	$$⊢\phi \to D\in K$$
15		lvecindp2.q	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
16		lvecindp2.e	$$⊢\phi \to \left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{·}Y\right)=\left(C\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(D\underset{\dot{}}{·}Y\right)$$
17		eqid	$$⊢\mathrm{Cntz}\left(W\right)=\mathrm{Cntz}\left(W\right)$$
18		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
19	8 18	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
20	9	eldifad	$$⊢\phi \to X\in V$$
21	1 7	lspsnsubg	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to N\left(\left\{X\right\}\right)\in \mathrm{SubGrp}\left(W\right)$$
22	19 20 21	syl2anc	$$⊢\phi \to N\left(\left\{X\right\}\right)\in \mathrm{SubGrp}\left(W\right)$$
23	10	eldifad	$$⊢\phi \to Y\in V$$
24	1 7	lspsnsubg	$$⊢\left(W\in \mathrm{LMod}\wedge Y\in V\right)\to N\left(\left\{Y\right\}\right)\in \mathrm{SubGrp}\left(W\right)$$
25	19 23 24	syl2anc	$$⊢\phi \to N\left(\left\{Y\right\}\right)\in \mathrm{SubGrp}\left(W\right)$$
26	1 6 7 8 20 23 15	lspdisj2	$$⊢\phi \to N\left(\left\{X\right\}\right)\cap N\left(\left\{Y\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
27		lmodabl	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$
28	19 27	syl	$$⊢\phi \to W\in \mathrm{Abel}$$
29	17 28 22 25	ablcntzd	$$⊢\phi \to N\left(\left\{X\right\}\right)\subseteq \mathrm{Cntz}\left(W\right)\left(N\left(\left\{Y\right\}\right)\right)$$
30	1 5 3 4 7 19 11 20	lspsneli	$$⊢\phi \to A\underset{\dot{}}{·}X\in N\left(\left\{X\right\}\right)$$
31	1 5 3 4 7 19 13 20	lspsneli	$$⊢\phi \to C\underset{\dot{}}{·}X\in N\left(\left\{X\right\}\right)$$
32	1 5 3 4 7 19 12 23	lspsneli	$$⊢\phi \to B\underset{\dot{}}{·}Y\in N\left(\left\{Y\right\}\right)$$
33	1 5 3 4 7 19 14 23	lspsneli	$$⊢\phi \to D\underset{\dot{}}{·}Y\in N\left(\left\{Y\right\}\right)$$
34	2 6 17 22 25 26 29 30 31 32 33	subgdisjb	$$⊢\phi \to \left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{·}Y\right)=\left(C\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(D\underset{\dot{}}{·}Y\right)\leftrightarrow \left(A\underset{\dot{}}{·}X=C\underset{\dot{}}{·}X\wedge B\underset{\dot{}}{·}Y=D\underset{\dot{}}{·}Y\right)\right)$$
35	16 34	mpbid	$$⊢\phi \to \left(A\underset{\dot{}}{·}X=C\underset{\dot{}}{·}X\wedge B\underset{\dot{}}{·}Y=D\underset{\dot{}}{·}Y\right)$$
36		eldifsni	$$⊢X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to X\ne \underset{\dot{}}{0}$$
37	9 36	syl	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
38	1 5 3 4 6 8 11 13 20 37	lvecvscan2	$$⊢\phi \to \left(A\underset{\dot{}}{·}X=C\underset{\dot{}}{·}X\leftrightarrow A=C\right)$$
39		eldifsni	$$⊢Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to Y\ne \underset{\dot{}}{0}$$
40	10 39	syl	$$⊢\phi \to Y\ne \underset{\dot{}}{0}$$
41	1 5 3 4 6 8 12 14 23 40	lvecvscan2	$$⊢\phi \to \left(B\underset{\dot{}}{·}Y=D\underset{\dot{}}{·}Y\leftrightarrow B=D\right)$$
42	38 41	anbi12d	$$⊢\phi \to \left(\left(A\underset{\dot{}}{·}X=C\underset{\dot{}}{·}X\wedge B\underset{\dot{}}{·}Y=D\underset{\dot{}}{·}Y\right)\leftrightarrow \left(A=C\wedge B=D\right)\right)$$
43	35 42	mpbid	$$⊢\phi \to \left(A=C\wedge B=D\right)$$