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

Metamath Proof Explorer

Theorem 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 
|- .+ = ( +g ` W )
lvecindp.f 
|- F = ( Scalar ` W )
lvecindp.k 
|- K = ( Base ` F )
lvecindp.t 
|- .x. = ( .s ` W )
lvecindp.s 
|- S = ( LSubSp ` W )
lvecindp.w 
|- ( ph -> W e. LVec )
lvecindp.u 
|- ( ph -> U e. S )
lvecindp.x 
|- ( ph -> X e. V )
lvecindp.n 
|- ( ph -> -. X e. U )
lvecindp.y 
|- ( ph -> Y e. U )
lvecindp.z 
|- ( ph -> Z e. U )
lvecindp.a 
|- ( ph -> A e. K )
lvecindp.b 
|- ( ph -> B e. K )
lvecindp.e 
|- ( ph -> ( ( A .x. X ) .+ Y ) = ( ( B .x. X ) .+ Z ) )
Assertion lvecindp 
|- ( ph -> ( A = B /\ Y = Z ) )

Proof

Step Hyp Ref Expression
1 lvecindp.v 
 |-  V = ( Base ` W )
2 lvecindp.p 
 |-  .+ = ( +g ` W )
3 lvecindp.f 
 |-  F = ( Scalar ` W )
4 lvecindp.k 
 |-  K = ( Base ` F )
5 lvecindp.t 
 |-  .x. = ( .s ` W )
6 lvecindp.s 
 |-  S = ( LSubSp ` W )
7 lvecindp.w 
 |-  ( ph -> W e. LVec )
8 lvecindp.u 
 |-  ( ph -> U e. S )
9 lvecindp.x 
 |-  ( ph -> X e. V )
10 lvecindp.n 
 |-  ( ph -> -. X e. U )
11 lvecindp.y 
 |-  ( ph -> Y e. U )
12 lvecindp.z 
 |-  ( ph -> Z e. U )
13 lvecindp.a 
 |-  ( ph -> A e. K )
14 lvecindp.b 
 |-  ( ph -> B e. K )
15 lvecindp.e 
 |-  ( ph -> ( ( A .x. X ) .+ Y ) = ( ( B .x. X ) .+ Z ) )
16 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
17 eqid 
 |-  ( Cntz ` W ) = ( Cntz ` W )
18 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
19 7 18 syl 
 |-  ( ph -> W e. LMod )
20 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
21 1 20 lspsnsubg 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( LSpan ` W ) ` { X } ) e. ( SubGrp ` W ) )
22 19 9 21 syl2anc 
 |-  ( ph -> ( ( LSpan ` W ) ` { X } ) e. ( SubGrp ` W ) )
23 6 lsssssubg 
 |-  ( W e. LMod -> S C_ ( SubGrp ` W ) )
24 19 23 syl 
 |-  ( ph -> S C_ ( SubGrp ` W ) )
25 24 8 sseldd 
 |-  ( ph -> U e. ( SubGrp ` W ) )
26 1 16 20 6 7 8 9 10 lspdisj 
 |-  ( ph -> ( ( ( LSpan ` W ) ` { X } ) i^i U ) = { ( 0g ` W ) } )
27 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
28 19 27 syl 
 |-  ( ph -> W e. Abel )
29 17 28 22 25 ablcntzd 
 |-  ( ph -> ( ( LSpan ` W ) ` { X } ) C_ ( ( Cntz ` W ) ` U ) )
30 1 5 3 4 20 19 13 9 ellspsni 
 |-  ( ph -> ( A .x. X ) e. ( ( LSpan ` W ) ` { X } ) )
31 1 5 3 4 20 19 14 9 ellspsni 
 |-  ( ph -> ( B .x. X ) e. ( ( LSpan ` W ) ` { X } ) )
32 2 16 17 22 25 26 29 30 31 11 12 15 subgdisj1 
 |-  ( ph -> ( A .x. X ) = ( B .x. X ) )
33 16 6 19 8 10 lssvneln0 
 |-  ( ph -> X =/= ( 0g ` W ) )
34 1 5 3 4 16 7 13 14 9 33 lvecvscan2 
 |-  ( ph -> ( ( A .x. X ) = ( B .x. X ) <-> A = B ) )
35 32 34 mpbid 
 |-  ( ph -> A = B )
36 2 16 17 22 25 26 29 30 31 11 12 15 subgdisj2 
 |-  ( ph -> Y = Z )
37 35 36 jca 
 |-  ( ph -> ( A = B /\ Y = Z ) )