Metamath Proof Explorer


Theorem lsmpr

Description: The span of a pair of vectors equals the sum of the spans of their singletons. (Contributed by NM, 13-Jan-2015)

Ref Expression
Hypotheses lsmpr.v V=BaseW
lsmpr.n N=LSpanW
lsmpr.p ˙=LSSumW
lsmpr.w φWLMod
lsmpr.x φXV
lsmpr.y φYV
Assertion lsmpr φNXY=NX˙NY

Proof

Step Hyp Ref Expression
1 lsmpr.v V=BaseW
2 lsmpr.n N=LSpanW
3 lsmpr.p ˙=LSSumW
4 lsmpr.w φWLMod
5 lsmpr.x φXV
6 lsmpr.y φYV
7 5 snssd φXV
8 6 snssd φYV
9 1 2 lspun WLModXVYVNXY=NNXNY
10 4 7 8 9 syl3anc φNXY=NNXNY
11 df-pr XY=XY
12 11 fveq2i NXY=NXY
13 12 a1i φNXY=NXY
14 eqid LSubSpW=LSubSpW
15 1 14 2 lspsncl WLModXVNXLSubSpW
16 4 5 15 syl2anc φNXLSubSpW
17 1 14 2 lspsncl WLModYVNYLSubSpW
18 4 6 17 syl2anc φNYLSubSpW
19 14 2 3 lsmsp WLModNXLSubSpWNYLSubSpWNX˙NY=NNXNY
20 4 16 18 19 syl3anc φNX˙NY=NNXNY
21 10 13 20 3eqtr4d φNXY=NX˙NY