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 
|- V = ( Base ` W )
lvecindp2.p 
|- .+ = ( +g ` W )
lvecindp2.f 
|- F = ( Scalar ` W )
lvecindp2.k 
|- K = ( Base ` F )
lvecindp2.t 
|- .x. = ( .s ` W )
lvecindp2.o 
|- .0. = ( 0g ` W )
lvecindp2.n 
|- N = ( LSpan ` W )
lvecindp2.w 
|- ( ph -> W e. LVec )
lvecindp2.x 
|- ( ph -> X e. ( V \ { .0. } ) )
lvecindp2.y 
|- ( ph -> Y e. ( V \ { .0. } ) )
lvecindp2.a 
|- ( ph -> A e. K )
lvecindp2.b 
|- ( ph -> B e. K )
lvecindp2.c 
|- ( ph -> C e. K )
lvecindp2.d 
|- ( ph -> D e. K )
lvecindp2.q 
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
lvecindp2.e 
|- ( ph -> ( ( A .x. X ) .+ ( B .x. Y ) ) = ( ( C .x. X ) .+ ( D .x. Y ) ) )
Assertion lvecindp2 
|- ( ph -> ( A = C /\ B = D ) )

Proof

Step Hyp Ref Expression
1 lvecindp2.v 
 |-  V = ( Base ` W )
2 lvecindp2.p 
 |-  .+ = ( +g ` W )
3 lvecindp2.f 
 |-  F = ( Scalar ` W )
4 lvecindp2.k 
 |-  K = ( Base ` F )
5 lvecindp2.t 
 |-  .x. = ( .s ` W )
6 lvecindp2.o 
 |-  .0. = ( 0g ` W )
7 lvecindp2.n 
 |-  N = ( LSpan ` W )
8 lvecindp2.w 
 |-  ( ph -> W e. LVec )
9 lvecindp2.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
10 lvecindp2.y 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
11 lvecindp2.a 
 |-  ( ph -> A e. K )
12 lvecindp2.b 
 |-  ( ph -> B e. K )
13 lvecindp2.c 
 |-  ( ph -> C e. K )
14 lvecindp2.d 
 |-  ( ph -> D e. K )
15 lvecindp2.q 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
16 lvecindp2.e 
 |-  ( ph -> ( ( A .x. X ) .+ ( B .x. Y ) ) = ( ( C .x. X ) .+ ( D .x. Y ) ) )
17 eqid 
 |-  ( Cntz ` W ) = ( Cntz ` W )
18 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
19 8 18 syl 
 |-  ( ph -> W e. LMod )
20 9 eldifad 
 |-  ( ph -> X e. V )
21 1 7 lspsnsubg 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( SubGrp ` W ) )
22 19 20 21 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ( SubGrp ` W ) )
23 10 eldifad 
 |-  ( ph -> Y e. V )
24 1 7 lspsnsubg 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( SubGrp ` W ) )
25 19 23 24 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( SubGrp ` W ) )
26 1 6 7 8 20 23 15 lspdisj2 
 |-  ( ph -> ( ( N ` { X } ) i^i ( N ` { Y } ) ) = { .0. } )
27 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
28 19 27 syl 
 |-  ( ph -> W e. Abel )
29 17 28 22 25 ablcntzd 
 |-  ( ph -> ( N ` { X } ) C_ ( ( Cntz ` W ) ` ( N ` { Y } ) ) )
30 1 5 3 4 7 19 11 20 ellspsni 
 |-  ( ph -> ( A .x. X ) e. ( N ` { X } ) )
31 1 5 3 4 7 19 13 20 ellspsni 
 |-  ( ph -> ( C .x. X ) e. ( N ` { X } ) )
32 1 5 3 4 7 19 12 23 ellspsni 
 |-  ( ph -> ( B .x. Y ) e. ( N ` { Y } ) )
33 1 5 3 4 7 19 14 23 ellspsni 
 |-  ( ph -> ( D .x. Y ) e. ( N ` { Y } ) )
34 2 6 17 22 25 26 29 30 31 32 33 subgdisjb 
 |-  ( ph -> ( ( ( A .x. X ) .+ ( B .x. Y ) ) = ( ( C .x. X ) .+ ( D .x. Y ) ) <-> ( ( A .x. X ) = ( C .x. X ) /\ ( B .x. Y ) = ( D .x. Y ) ) ) )
35 16 34 mpbid 
 |-  ( ph -> ( ( A .x. X ) = ( C .x. X ) /\ ( B .x. Y ) = ( D .x. Y ) ) )
36 eldifsni 
 |-  ( X e. ( V \ { .0. } ) -> X =/= .0. )
37 9 36 syl 
 |-  ( ph -> X =/= .0. )
38 1 5 3 4 6 8 11 13 20 37 lvecvscan2 
 |-  ( ph -> ( ( A .x. X ) = ( C .x. X ) <-> A = C ) )
39 eldifsni 
 |-  ( Y e. ( V \ { .0. } ) -> Y =/= .0. )
40 10 39 syl 
 |-  ( ph -> Y =/= .0. )
41 1 5 3 4 6 8 12 14 23 40 lvecvscan2 
 |-  ( ph -> ( ( B .x. Y ) = ( D .x. Y ) <-> B = D ) )
42 38 41 anbi12d 
 |-  ( ph -> ( ( ( A .x. X ) = ( C .x. X ) /\ ( B .x. Y ) = ( D .x. Y ) ) <-> ( A = C /\ B = D ) ) )
43 35 42 mpbid 
 |-  ( ph -> ( A = C /\ B = D ) )