lvecindp2

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

	Ref	Expression
Hypotheses	lvecindp2.v	$⊢ V = {Base}_{W}$
	lvecindp2.p	$⊢ \underset{˙}{+} = +_{W}$
	lvecindp2.f	$⊢ F = Scalar (W)$
	lvecindp2.k	$⊢ K = {Base}_{F}$
	lvecindp2.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lvecindp2.o	$⊢ \underset{˙}{0} = 0_{W}$
	lvecindp2.n	$⊢ N = LSpan (W)$
	lvecindp2.w	$⊢ φ \to W \in LVec$
	lvecindp2.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	lvecindp2.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	lvecindp2.a	$⊢ φ \to A \in K$
	lvecindp2.b	$⊢ φ \to B \in K$
	lvecindp2.c	$⊢ φ \to C \in K$
	lvecindp2.d	$⊢ φ \to D \in K$
	lvecindp2.q	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	lvecindp2.e	$⊢ φ \to (A \underset{˙}{\cdot} X) \underset{˙}{+} (B \underset{˙}{\cdot} Y) = (C \underset{˙}{\cdot} X) \underset{˙}{+} (D \underset{˙}{\cdot} Y)$
Assertion	lvecindp2	$⊢ φ \to (A = C \land B = D)$

Proof

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

Metamath Proof Explorer

Theorem lvecindp2

Proof