Metamath Proof Explorer


Theorem lsatfixedN

Description: Show equality with the span of the sum of two vectors, one of which ( X ) is fixed in advance. Compare lspfixed . (Contributed by NM, 29-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lsatfixed.v V = Base W
lsatfixed.p + ˙ = + W
lsatfixed.o 0 ˙ = 0 W
lsatfixed.n N = LSpan W
lsatfixed.a A = LSAtoms W
lsatfixed.w φ W LVec
lsatfixed.q φ Q A
lsatfixed.x φ X V
lsatfixed.y φ Y V
lsatfixed.e φ Q N X
lsatfixed.f φ Q N Y
lsatfixed.g φ Q N X Y
Assertion lsatfixedN φ z N Y 0 ˙ Q = N X + ˙ z

Proof

Step Hyp Ref Expression
1 lsatfixed.v V = Base W
2 lsatfixed.p + ˙ = + W
3 lsatfixed.o 0 ˙ = 0 W
4 lsatfixed.n N = LSpan W
5 lsatfixed.a A = LSAtoms W
6 lsatfixed.w φ W LVec
7 lsatfixed.q φ Q A
8 lsatfixed.x φ X V
9 lsatfixed.y φ Y V
10 lsatfixed.e φ Q N X
11 lsatfixed.f φ Q N Y
12 lsatfixed.g φ Q N X Y
13 1 4 3 5 islsat W LVec Q A w V 0 ˙ Q = N w
14 6 13 syl φ Q A w V 0 ˙ Q = N w
15 7 14 mpbid φ w V 0 ˙ Q = N w
16 6 3ad2ant1 φ w V 0 ˙ Q = N w W LVec
17 8 3ad2ant1 φ w V 0 ˙ Q = N w X V
18 9 3ad2ant1 φ w V 0 ˙ Q = N w Y V
19 simp2 φ w V 0 ˙ Q = N w w V 0 ˙
20 simp3 φ w V 0 ˙ Q = N w Q = N w
21 20 eqcomd φ w V 0 ˙ Q = N w N w = Q
22 10 3ad2ant1 φ w V 0 ˙ Q = N w Q N X
23 21 22 eqnetrd φ w V 0 ˙ Q = N w N w N X
24 1 3 4 16 19 17 23 lspsnne1 φ w V 0 ˙ Q = N w ¬ w N X
25 11 3ad2ant1 φ w V 0 ˙ Q = N w Q N Y
26 21 25 eqnetrd φ w V 0 ˙ Q = N w N w N Y
27 1 3 4 16 19 18 26 lspsnne1 φ w V 0 ˙ Q = N w ¬ w N Y
28 12 3ad2ant1 φ w V 0 ˙ Q = N w Q N X Y
29 21 28 eqsstrd φ w V 0 ˙ Q = N w N w N X Y
30 eqid LSubSp W = LSubSp W
31 lveclmod W LVec W LMod
32 6 31 syl φ W LMod
33 32 3ad2ant1 φ w V 0 ˙ Q = N w W LMod
34 1 30 4 32 8 9 lspprcl φ N X Y LSubSp W
35 34 3ad2ant1 φ w V 0 ˙ Q = N w N X Y LSubSp W
36 19 eldifad φ w V 0 ˙ Q = N w w V
37 1 30 4 33 35 36 lspsnel5 φ w V 0 ˙ Q = N w w N X Y N w N X Y
38 29 37 mpbird φ w V 0 ˙ Q = N w w N X Y
39 1 2 3 4 16 17 18 24 27 38 lspfixed φ w V 0 ˙ Q = N w z N Y 0 ˙ w N X + ˙ z
40 simpl1 φ w V 0 ˙ Q = N w z N Y 0 ˙ φ
41 40 6 syl φ w V 0 ˙ Q = N w z N Y 0 ˙ W LVec
42 simpl2 φ w V 0 ˙ Q = N w z N Y 0 ˙ w V 0 ˙
43 40 32 syl φ w V 0 ˙ Q = N w z N Y 0 ˙ W LMod
44 40 8 syl φ w V 0 ˙ Q = N w z N Y 0 ˙ X V
45 9 snssd φ Y V
46 1 4 lspssv W LMod Y V N Y V
47 32 45 46 syl2anc φ N Y V
48 47 ssdifssd φ N Y 0 ˙ V
49 48 3ad2ant1 φ w V 0 ˙ Q = N w N Y 0 ˙ V
50 49 sselda φ w V 0 ˙ Q = N w z N Y 0 ˙ z V
51 1 2 lmodvacl W LMod X V z V X + ˙ z V
52 43 44 50 51 syl3anc φ w V 0 ˙ Q = N w z N Y 0 ˙ X + ˙ z V
53 1 3 4 41 42 52 lspsncmp φ w V 0 ˙ Q = N w z N Y 0 ˙ N w N X + ˙ z N w = N X + ˙ z
54 1 30 4 lspsncl W LMod X + ˙ z V N X + ˙ z LSubSp W
55 43 52 54 syl2anc φ w V 0 ˙ Q = N w z N Y 0 ˙ N X + ˙ z LSubSp W
56 42 eldifad φ w V 0 ˙ Q = N w z N Y 0 ˙ w V
57 1 30 4 43 55 56 lspsnel5 φ w V 0 ˙ Q = N w z N Y 0 ˙ w N X + ˙ z N w N X + ˙ z
58 simpl3 φ w V 0 ˙ Q = N w z N Y 0 ˙ Q = N w
59 58 eqeq1d φ w V 0 ˙ Q = N w z N Y 0 ˙ Q = N X + ˙ z N w = N X + ˙ z
60 53 57 59 3bitr4rd φ w V 0 ˙ Q = N w z N Y 0 ˙ Q = N X + ˙ z w N X + ˙ z
61 60 rexbidva φ w V 0 ˙ Q = N w z N Y 0 ˙ Q = N X + ˙ z z N Y 0 ˙ w N X + ˙ z
62 39 61 mpbird φ w V 0 ˙ Q = N w z N Y 0 ˙ Q = N X + ˙ z
63 62 rexlimdv3a φ w V 0 ˙ Q = N w z N Y 0 ˙ Q = N X + ˙ z
64 15 63 mpd φ z N Y 0 ˙ Q = N X + ˙ z