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 = Base W
lsppreli.p + ˙ = + W
lsppreli.t · ˙ = W
lsppreli.f F = Scalar W
lsppreli.k K = Base F
lsppreli.n N = LSpan W
lsppreli.w φ W LMod
lsppreli.a φ A K
lsppreli.b φ B K
lsppreli.x φ X V
lsppreli.y φ Y V
Assertion lsppreli φ A · ˙ X + ˙ B · ˙ Y N X Y

Proof

Step Hyp Ref Expression
1 lsppreli.v V = Base W
2 lsppreli.p + ˙ = + W
3 lsppreli.t · ˙ = W
4 lsppreli.f F = Scalar W
5 lsppreli.k K = Base F
6 lsppreli.n N = LSpan W
7 lsppreli.w φ W LMod
8 lsppreli.a φ A K
9 lsppreli.b φ B K
10 lsppreli.x φ X V
11 lsppreli.y φ Y V
12 1 6 lspsnsubg W LMod X V N X SubGrp W
13 7 10 12 syl2anc φ N X SubGrp W
14 1 6 lspsnsubg W LMod Y V N Y SubGrp W
15 7 11 14 syl2anc φ N Y SubGrp W
16 1 3 4 5 6 7 8 10 lspsneli φ A · ˙ X N X
17 1 3 4 5 6 7 9 11 lspsneli φ B · ˙ Y N Y
18 eqid LSSum W = LSSum W
19 2 18 lsmelvali N X SubGrp W N Y SubGrp W A · ˙ X N X B · ˙ Y N Y A · ˙ X + ˙ B · ˙ Y N X LSSum W N Y
20 13 15 16 17 19 syl22anc φ A · ˙ X + ˙ B · ˙ Y N X LSSum W N Y
21 1 6 18 7 10 11 lsmpr φ N X Y = N X LSSum W N Y
22 20 21 eleqtrrd φ A · ˙ X + ˙ B · ˙ Y N X Y