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 ⊢ 𝑉 = ( 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 lspsneli ⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) )
31 1 5 3 4 20 19 14 9 lspsneli ⊢ ( 𝜑 → ( 𝐵 · 𝑋 ) ∈ ( ( 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 ⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∧ 𝑌 = 𝑍 ) )