Metamath Proof Explorer


Theorem lsppreli

Description: A vector expressed as a sum belongs to the span of its components. (Contributed by NM, 9-Apr-2015)

Ref Expression
Hypotheses lsppreli.v V=BaseW
lsppreli.p +˙=+W
lsppreli.t ·˙=W
lsppreli.f F=ScalarW
lsppreli.k K=BaseF
lsppreli.n N=LSpanW
lsppreli.w φWLMod
lsppreli.a φAK
lsppreli.b φBK
lsppreli.x φXV
lsppreli.y φYV
Assertion lsppreli φA·˙X+˙B·˙YNXY

Proof

Step Hyp Ref Expression
1 lsppreli.v V=BaseW
2 lsppreli.p +˙=+W
3 lsppreli.t ·˙=W
4 lsppreli.f F=ScalarW
5 lsppreli.k K=BaseF
6 lsppreli.n N=LSpanW
7 lsppreli.w φWLMod
8 lsppreli.a φAK
9 lsppreli.b φBK
10 lsppreli.x φXV
11 lsppreli.y φYV
12 1 6 lspsnsubg WLModXVNXSubGrpW
13 7 10 12 syl2anc φNXSubGrpW
14 1 6 lspsnsubg WLModYVNYSubGrpW
15 7 11 14 syl2anc φNYSubGrpW
16 1 3 4 5 6 7 8 10 lspsneli φA·˙XNX
17 1 3 4 5 6 7 9 11 lspsneli φB·˙YNY
18 eqid LSSumW=LSSumW
19 2 18 lsmelvali NXSubGrpWNYSubGrpWA·˙XNXB·˙YNYA·˙X+˙B·˙YNXLSSumWNY
20 13 15 16 17 19 syl22anc φA·˙X+˙B·˙YNXLSSumWNY
21 1 6 18 7 10 11 lsmpr φNXY=NXLSSumWNY
22 20 21 eleqtrrd φA·˙X+˙B·˙YNXY