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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lvecindp.p	⊢ + = ( +g ‘ 𝑊 )
	lvecindp.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lvecindp.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	lvecindp.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lvecindp.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lvecindp.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lvecindp.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lvecindp.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lvecindp.n	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
	lvecindp.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
	lvecindp.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
	lvecindp.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
	lvecindp.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
	lvecindp.e	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) + 𝑌 ) = ( ( 𝐵 · 𝑋 ) + 𝑍 ) )
Assertion	lvecindp	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∧ 𝑌 = 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		lvecindp.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lvecindp.p	⊢ + = ( +g ‘ 𝑊 )
3		lvecindp.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4		lvecindp.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
5		lvecindp.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		lvecindp.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
7		lvecindp.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
8		lvecindp.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
9		lvecindp.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10		lvecindp.n	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
11		lvecindp.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
12		lvecindp.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
13		lvecindp.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
14		lvecindp.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
15		lvecindp.e	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) + 𝑌 ) = ( ( 𝐵 · 𝑋 ) + 𝑍 ) )
16		eqid	⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
17		eqid	⊢ ( Cntz ‘ 𝑊 ) = ( Cntz ‘ 𝑊 )
18		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
19	7 18	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
20		eqid	⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
21	1 20	lspsnsubg	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
22	19 9 21	syl2anc	⊢ ( 𝜑 → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
23	6	lsssssubg	⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
24	19 23	syl	⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
25	24 8	sseldd	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
26	1 16 20 6 7 8 9 10	lspdisj	⊢ ( 𝜑 → ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) ∩ 𝑈 ) = { ( 0g ‘ 𝑊 ) } )
27		lmodabl	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
28	19 27	syl	⊢ ( 𝜑 → 𝑊 ∈ Abel )
29	17 28 22 25	ablcntzd	⊢ ( 𝜑 → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) ⊆ ( ( Cntz ‘ 𝑊 ) ‘ 𝑈 ) )
30	1 5 3 4 20 19 13 9	ellspsni	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) )
31	1 5 3 4 20 19 14 9	ellspsni	⊢ ( 𝜑 → ( 𝐵 · 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) )
32	2 16 17 22 25 26 29 30 31 11 12 15	subgdisj1	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) = ( 𝐵 · 𝑋 ) )
33	16 6 19 8 10	lssvneln0	⊢ ( 𝜑 → 𝑋 ≠ ( 0g ‘ 𝑊 ) )
34	1 5 3 4 16 7 13 14 9 33	lvecvscan2	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) = ( 𝐵 · 𝑋 ) ↔ 𝐴 = 𝐵 ) )
35	32 34	mpbid	⊢ ( 𝜑 → 𝐴 = 𝐵 )
36	2 16 17 22 25 26 29 30 31 11 12 15	subgdisj2	⊢ ( 𝜑 → 𝑌 = 𝑍 )
37	35 36	jca	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∧ 𝑌 = 𝑍 ) )