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 = {Base}_{W}$
	lvecindp.p	$⊢ \underset{˙}{+} = +_{W}$
	lvecindp.f	$⊢ F = Scalar (W)$
	lvecindp.k	$⊢ K = {Base}_{F}$
	lvecindp.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lvecindp.s	$⊢ S = LSubSp (W)$
	lvecindp.w	$⊢ φ \to W \in LVec$
	lvecindp.u	$⊢ φ \to U \in S$
	lvecindp.x	$⊢ φ \to X \in V$
	lvecindp.n	$⊢ φ \to \neg X \in U$
	lvecindp.y	$⊢ φ \to Y \in U$
	lvecindp.z	$⊢ φ \to Z \in U$
	lvecindp.a	$⊢ φ \to A \in K$
	lvecindp.b	$⊢ φ \to B \in K$
	lvecindp.e	$⊢ φ \to (A \underset{˙}{\cdot} X) \underset{˙}{+} Y = (B \underset{˙}{\cdot} X) \underset{˙}{+} Z$
Assertion	lvecindp	$⊢ φ \to (A = B \land Y = Z)$

Proof

Step	Hyp	Ref	Expression
1		lvecindp.v	$⊢ V = {Base}_{W}$
2		lvecindp.p	$⊢ \underset{˙}{+} = +_{W}$
3		lvecindp.f	$⊢ F = Scalar (W)$
4		lvecindp.k	$⊢ K = {Base}_{F}$
5		lvecindp.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		lvecindp.s	$⊢ S = LSubSp (W)$
7		lvecindp.w	$⊢ φ \to W \in LVec$
8		lvecindp.u	$⊢ φ \to U \in S$
9		lvecindp.x	$⊢ φ \to X \in V$
10		lvecindp.n	$⊢ φ \to \neg X \in U$
11		lvecindp.y	$⊢ φ \to Y \in U$
12		lvecindp.z	$⊢ φ \to Z \in U$
13		lvecindp.a	$⊢ φ \to A \in K$
14		lvecindp.b	$⊢ φ \to B \in K$
15		lvecindp.e	$⊢ φ \to (A \underset{˙}{\cdot} X) \underset{˙}{+} Y = (B \underset{˙}{\cdot} X) \underset{˙}{+} Z$
16		eqid	$⊢ 0_{W} = 0_{W}$
17		eqid	$⊢ Cntz (W) = Cntz (W)$
18		lveclmod	$⊢ W \in LVec \to W \in LMod$
19	7 18	syl	$⊢ φ \to W \in LMod$
20		eqid	$⊢ LSpan (W) = LSpan (W)$
21	1 20	lspsnsubg	$⊢ (W \in LMod \land X \in V) \to LSpan (W) (\{X\}) \in SubGrp (W)$
22	19 9 21	syl2anc	$⊢ φ \to LSpan (W) (\{X\}) \in SubGrp (W)$
23	6	lsssssubg	$⊢ W \in LMod \to S \subseteq SubGrp (W)$
24	19 23	syl	$⊢ φ \to S \subseteq SubGrp (W)$
25	24 8	sseldd	$⊢ φ \to U \in SubGrp (W)$
26	1 16 20 6 7 8 9 10	lspdisj	$⊢ φ \to LSpan (W) (\{X\}) \cap U = \{0_{W}\}$
27		lmodabl	$⊢ W \in LMod \to W \in Abel$
28	19 27	syl	$⊢ φ \to W \in Abel$
29	17 28 22 25	ablcntzd	$⊢ φ \to LSpan (W) (\{X\}) \subseteq Cntz (W) (U)$
30	1 5 3 4 20 19 13 9	ellspsni	$⊢ φ \to A \underset{˙}{\cdot} X \in LSpan (W) (\{X\})$
31	1 5 3 4 20 19 14 9	ellspsni	$⊢ φ \to B \underset{˙}{\cdot} X \in LSpan (W) (\{X\})$
32	2 16 17 22 25 26 29 30 31 11 12 15	subgdisj1	$⊢ φ \to A \underset{˙}{\cdot} X = B \underset{˙}{\cdot} X$
33	16 6 19 8 10	lssvneln0	$⊢ φ \to X \neq 0_{W}$
34	1 5 3 4 16 7 13 14 9 33	lvecvscan2	$⊢ φ \to (A \underset{˙}{\cdot} X = B \underset{˙}{\cdot} X \leftrightarrow A = B)$
35	32 34	mpbid	$⊢ φ \to A = B$
36	2 16 17 22 25 26 29 30 31 11 12 15	subgdisj2	$⊢ φ \to Y = Z$
37	35 36	jca	$⊢ φ \to (A = B \land Y = Z)$

Metamath Proof Explorer

Theorem lvecindp

Proof