This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )