Theorem lvecindp

Description: Compute the X coefficient in a sum with an independent vector X (first conjunct), which can then be removed to continue with the remaining vectors summed in expressions Y and Z (second conjunct). Typically, U is the span of the remaining vectors. (Contributed by NM, 5-Apr-2015) (Revised by Mario Carneiro, 21-Apr-2016) (Proof shortened by AV, 19-Jul-2022)

	Ref	Expression
Hypotheses	lvecindp.v	$$⊢V={\mathrm{Base}}_W$$
	lvecindp.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	lvecindp.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lvecindp.k	$$⊢K={\mathrm{Base}}_F$$
	lvecindp.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lvecindp.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lvecindp.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lvecindp.u	$$⊢\phi \to U\in S$$
	lvecindp.x	$$⊢\phi \to X\in V$$
	lvecindp.n	$$⊢\phi \to \neg X\in U$$
	lvecindp.y	$$⊢\phi \to Y\in U$$
	lvecindp.z	$$⊢\phi \to Z\in U$$
	lvecindp.a	$$⊢\phi \to A\in K$$
	lvecindp.b	$$⊢\phi \to B\in K$$
	lvecindp.e	$$⊢\phi \to \left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}Y=\left(B\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}Z$$
Assertion	lvecindp	$$⊢\phi \to \left(A=B\wedge Y=Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		lvecindp.v	$$⊢V={\mathrm{Base}}_W$$
2		lvecindp.p	$$⊢\underset{\dot{}}{+}={+}_W$$
3		lvecindp.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		lvecindp.k	$$⊢K={\mathrm{Base}}_F$$
5		lvecindp.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		lvecindp.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
7		lvecindp.w	$$⊢\phi \to W\in \mathrm{LVec}$$
8		lvecindp.u	$$⊢\phi \to U\in S$$
9		lvecindp.x	$$⊢\phi \to X\in V$$
10		lvecindp.n	$$⊢\phi \to \neg X\in U$$
11		lvecindp.y	$$⊢\phi \to Y\in U$$
12		lvecindp.z	$$⊢\phi \to Z\in U$$
13		lvecindp.a	$$⊢\phi \to A\in K$$
14		lvecindp.b	$$⊢\phi \to B\in K$$
15		lvecindp.e	$$⊢\phi \to \left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}Y=\left(B\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}Z$$
16		eqid	$$⊢0_W=0_W$$
17		eqid	$$⊢\mathrm{Cntz}\left(W\right)=\mathrm{Cntz}\left(W\right)$$
18		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
19	7 18	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
20		eqid	$$⊢\mathrm{LSpan}\left(W\right)=\mathrm{LSpan}\left(W\right)$$
21	1 20	lspsnsubg	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\right)\in \mathrm{SubGrp}\left(W\right)$$
22	19 9 21	syl2anc	$$⊢\phi \to \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\right)\in \mathrm{SubGrp}\left(W\right)$$
23	6	lsssssubg	$$⊢W\in \mathrm{LMod}\to S\subseteq \mathrm{SubGrp}\left(W\right)$$
24	19 23	syl	$$⊢\phi \to S\subseteq \mathrm{SubGrp}\left(W\right)$$
25	24 8	sseldd	$$⊢\phi \to U\in \mathrm{SubGrp}\left(W\right)$$
26	1 16 20 6 7 8 9 10	lspdisj	$$⊢\phi \to \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\right)\cap U=\left\{0_W\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 \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\right)\subseteq \mathrm{Cntz}\left(W\right)\left(U\right)$$
30	1 5 3 4 20 19 13 9	lspsneli	$$⊢\phi \to A\underset{\dot{}}{·}X\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\right)$$
31	1 5 3 4 20 19 14 9	lspsneli	$$⊢\phi \to B\underset{\dot{}}{·}X\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\right)$$
32	2 16 17 22 25 26 29 30 31 11 12 15	subgdisj1	$$⊢\phi \to A\underset{\dot{}}{·}X=B\underset{\dot{}}{·}X$$
33	16 6 19 8 10	lssvneln0	$$⊢\phi \to X\ne 0_W$$
34	1 5 3 4 16 7 13 14 9 33	lvecvscan2	$$⊢\phi \to \left(A\underset{\dot{}}{·}X=B\underset{\dot{}}{·}X\leftrightarrow A=B\right)$$
35	32 34	mpbid	$$⊢\phi \to A=B$$
36	2 16 17 22 25 26 29 30 31 11 12 15	subgdisj2	$$⊢\phi \to Y=Z$$
37	35 36	jca	$$⊢\phi \to \left(A=B\wedge Y=Z\right)$$