Metamath Proof Explorer


Theorem lspabs2

Description: Absorption law for span of vector sum. (Contributed by NM, 30-Apr-2015)

Ref Expression
Hypotheses lspabs2.v V = Base W
lspabs2.p + ˙ = + W
lspabs2.o 0 ˙ = 0 W
lspabs2.n N = LSpan W
lspabs2.w φ W LVec
lspabs2.x φ X V
lspabs2.y φ Y V 0 ˙
lspabs2.e φ N X = N X + ˙ Y
Assertion lspabs2 φ N X = N Y

Proof

Step Hyp Ref Expression
1 lspabs2.v V = Base W
2 lspabs2.p + ˙ = + W
3 lspabs2.o 0 ˙ = 0 W
4 lspabs2.n N = LSpan W
5 lspabs2.w φ W LVec
6 lspabs2.x φ X V
7 lspabs2.y φ Y V 0 ˙
8 lspabs2.e φ N X = N X + ˙ Y
9 lveclmod W LVec W LMod
10 5 9 syl φ W LMod
11 1 4 lspsnsubg W LMod X V N X SubGrp W
12 10 6 11 syl2anc φ N X SubGrp W
13 7 eldifad φ Y V
14 1 4 lspsnsubg W LMod Y V N Y SubGrp W
15 10 13 14 syl2anc φ N Y SubGrp W
16 eqid LSSum W = LSSum W
17 16 lsmub2 N X SubGrp W N Y SubGrp W N Y N X LSSum W N Y
18 12 15 17 syl2anc φ N Y N X LSSum W N Y
19 8 oveq2d φ N X LSSum W N X = N X LSSum W N X + ˙ Y
20 16 lsmidm N X SubGrp W N X LSSum W N X = N X
21 12 20 syl φ N X LSSum W N X = N X
22 1 2 4 10 6 13 lspprabs φ N X X + ˙ Y = N X Y
23 1 2 lmodvacl W LMod X V Y V X + ˙ Y V
24 10 6 13 23 syl3anc φ X + ˙ Y V
25 1 4 16 10 6 24 lsmpr φ N X X + ˙ Y = N X LSSum W N X + ˙ Y
26 1 4 16 10 6 13 lsmpr φ N X Y = N X LSSum W N Y
27 22 25 26 3eqtr3d φ N X LSSum W N X + ˙ Y = N X LSSum W N Y
28 19 21 27 3eqtr3rd φ N X LSSum W N Y = N X
29 18 28 sseqtrd φ N Y N X
30 1 3 4 5 7 6 lspsncmp φ N Y N X N Y = N X
31 29 30 mpbid φ N Y = N X
32 31 eqcomd φ N X = N Y