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}={\mathrm{Base}}_{{W}}$
lvecindp.p
lvecindp.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
lvecindp.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
lvecindp.t
lvecindp.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
lvecindp.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
lvecindp.u ${⊢}{\phi }\to {U}\in {S}$
lvecindp.x ${⊢}{\phi }\to {X}\in {V}$
lvecindp.n ${⊢}{\phi }\to ¬{X}\in {U}$
lvecindp.y ${⊢}{\phi }\to {Y}\in {U}$
lvecindp.z ${⊢}{\phi }\to {Z}\in {U}$
lvecindp.a ${⊢}{\phi }\to {A}\in {K}$
lvecindp.b ${⊢}{\phi }\to {B}\in {K}$
lvecindp.e
Assertion lvecindp ${⊢}{\phi }\to \left({A}={B}\wedge {Y}={Z}\right)$

Proof

Step Hyp Ref Expression
1 lvecindp.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lvecindp.p
3 lvecindp.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
4 lvecindp.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
5 lvecindp.t
6 lvecindp.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
7 lvecindp.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
8 lvecindp.u ${⊢}{\phi }\to {U}\in {S}$
9 lvecindp.x ${⊢}{\phi }\to {X}\in {V}$
10 lvecindp.n ${⊢}{\phi }\to ¬{X}\in {U}$
11 lvecindp.y ${⊢}{\phi }\to {Y}\in {U}$
12 lvecindp.z ${⊢}{\phi }\to {Z}\in {U}$
13 lvecindp.a ${⊢}{\phi }\to {A}\in {K}$
14 lvecindp.b ${⊢}{\phi }\to {B}\in {K}$
15 lvecindp.e
16 eqid ${⊢}{0}_{{W}}={0}_{{W}}$
17 eqid ${⊢}\mathrm{Cntz}\left({W}\right)=\mathrm{Cntz}\left({W}\right)$
18 lveclmod ${⊢}{W}\in \mathrm{LVec}\to {W}\in \mathrm{LMod}$
19 7 18 syl ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
20 eqid ${⊢}\mathrm{LSpan}\left({W}\right)=\mathrm{LSpan}\left({W}\right)$
21 1 20 lspsnsubg ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to \mathrm{LSpan}\left({W}\right)\left(\left\{{X}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)$
22 19 9 21 syl2anc ${⊢}{\phi }\to \mathrm{LSpan}\left({W}\right)\left(\left\{{X}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)$
23 6 lsssssubg ${⊢}{W}\in \mathrm{LMod}\to {S}\subseteq \mathrm{SubGrp}\left({W}\right)$
24 19 23 syl ${⊢}{\phi }\to {S}\subseteq \mathrm{SubGrp}\left({W}\right)$
25 24 8 sseldd ${⊢}{\phi }\to {U}\in \mathrm{SubGrp}\left({W}\right)$
26 1 16 20 6 7 8 9 10 lspdisj ${⊢}{\phi }\to \mathrm{LSpan}\left({W}\right)\left(\left\{{X}\right\}\right)\cap {U}=\left\{{0}_{{W}}\right\}$
27 lmodabl ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{Abel}$
28 19 27 syl ${⊢}{\phi }\to {W}\in \mathrm{Abel}$
29 17 28 22 25 ablcntzd ${⊢}{\phi }\to \mathrm{LSpan}\left({W}\right)\left(\left\{{X}\right\}\right)\subseteq \mathrm{Cntz}\left({W}\right)\left({U}\right)$
30 1 5 3 4 20 19 13 9 lspsneli
31 1 5 3 4 20 19 14 9 lspsneli
32 2 16 17 22 25 26 29 30 31 11 12 15 subgdisj1
33 16 6 19 8 10 lssvneln0 ${⊢}{\phi }\to {X}\ne {0}_{{W}}$
34 1 5 3 4 16 7 13 14 9 33 lvecvscan2
35 32 34 mpbid ${⊢}{\phi }\to {A}={B}$
36 2 16 17 22 25 26 29 30 31 11 12 15 subgdisj2 ${⊢}{\phi }\to {Y}={Z}$
37 35 36 jca ${⊢}{\phi }\to \left({A}={B}\wedge {Y}={Z}\right)$