Theorem lvecindp2

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

	Ref	Expression
Hypotheses	lvecindp2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lvecindp2.p	⊢ + = ( +g ‘ 𝑊 )
	lvecindp2.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lvecindp2.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	lvecindp2.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lvecindp2.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lvecindp2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lvecindp2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lvecindp2.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
	lvecindp2.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
	lvecindp2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
	lvecindp2.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
	lvecindp2.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
	lvecindp2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝐾 )
	lvecindp2.q	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
	lvecindp2.e	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐶 · 𝑋 ) + ( 𝐷 · 𝑌 ) ) )
Assertion	lvecindp2	⊢ ( 𝜑 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		lvecindp2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lvecindp2.p	⊢ + = ( +g ‘ 𝑊 )
3		lvecindp2.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4		lvecindp2.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
5		lvecindp2.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		lvecindp2.o	⊢ 0 = ( 0g ‘ 𝑊 )
7		lvecindp2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
8		lvecindp2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
9		lvecindp2.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
10		lvecindp2.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
11		lvecindp2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
12		lvecindp2.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
13		lvecindp2.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
14		lvecindp2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝐾 )
15		lvecindp2.q	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
16		lvecindp2.e	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐶 · 𝑋 ) + ( 𝐷 · 𝑌 ) ) )
17		eqid	⊢ ( Cntz ‘ 𝑊 ) = ( Cntz ‘ 𝑊 )
18		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
19	8 18	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
20	9	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
21	1 7	lspsnsubg	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
22	19 20 21	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
23	10	eldifad	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
24	1 7	lspsnsubg	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) )
25	19 23 24	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) )
26	1 6 7 8 20 23 15	lspdisj2	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∩ ( 𝑁 ‘ { 𝑌 } ) ) = { 0 } )
27		lmodabl	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
28	19 27	syl	⊢ ( 𝜑 → 𝑊 ∈ Abel )
29	17 28 22 25	ablcntzd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( Cntz ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝑌 } ) ) )
30	1 5 3 4 7 19 11 20	ellspsni	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 } ) )
31	1 5 3 4 7 19 13 20	ellspsni	⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 } ) )
32	1 5 3 4 7 19 12 23	ellspsni	⊢ ( 𝜑 → ( 𝐵 · 𝑌 ) ∈ ( 𝑁 ‘ { 𝑌 } ) )
33	1 5 3 4 7 19 14 23	ellspsni	⊢ ( 𝜑 → ( 𝐷 · 𝑌 ) ∈ ( 𝑁 ‘ { 𝑌 } ) )
34	2 6 17 22 25 26 29 30 31 32 33	subgdisjb	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐶 · 𝑋 ) + ( 𝐷 · 𝑌 ) ) ↔ ( ( 𝐴 · 𝑋 ) = ( 𝐶 · 𝑋 ) ∧ ( 𝐵 · 𝑌 ) = ( 𝐷 · 𝑌 ) ) ) )
35	16 34	mpbid	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) = ( 𝐶 · 𝑋 ) ∧ ( 𝐵 · 𝑌 ) = ( 𝐷 · 𝑌 ) ) )
36		eldifsni	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) → 𝑋 ≠ 0 )
37	9 36	syl	⊢ ( 𝜑 → 𝑋 ≠ 0 )
38	1 5 3 4 6 8 11 13 20 37	lvecvscan2	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) = ( 𝐶 · 𝑋 ) ↔ 𝐴 = 𝐶 ) )
39		eldifsni	⊢ ( 𝑌 ∈ ( 𝑉 ∖ { 0 } ) → 𝑌 ≠ 0 )
40	10 39	syl	⊢ ( 𝜑 → 𝑌 ≠ 0 )
41	1 5 3 4 6 8 12 14 23 40	lvecvscan2	⊢ ( 𝜑 → ( ( 𝐵 · 𝑌 ) = ( 𝐷 · 𝑌 ) ↔ 𝐵 = 𝐷 ) )
42	38 41	anbi12d	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝑋 ) = ( 𝐶 · 𝑋 ) ∧ ( 𝐵 · 𝑌 ) = ( 𝐷 · 𝑌 ) ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
43	35 42	mpbid	⊢ ( 𝜑 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )