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	lspsneli	\|- ( ph -> ( A .x. X ) e. ( ( LSpan ` W ) ` { X } ) )
31	1 5 3 4 20 19 14 9	lspsneli	\|- ( 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 ) )

Metamath Proof Explorer

Theorem lvecindp

Proof