Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  lssvancl1 Structured version   Unicode version

Theorem lssvancl1 16022
 Description: Non-closure: if one vector belongs to a subspace but another does not, their sum does not belong. Useful for obtaining a new vector not in a subspace. TODO: notice similarity to lspindp3 16209. Can it be used along with lspsnne1 16190, lspsnne2 16191 to shorten this proof? (Contributed by NM, 14-May-2015.)
Hypotheses
Ref Expression
lssvancl.v
lssvancl.p
lssvancl.s
lssvancl.w
lssvancl.u
lssvancl.x
lssvancl.y
lssvancl.n
Assertion
Ref Expression
lssvancl1

Proof of Theorem lssvancl1
StepHypRef Expression
1 lssvancl.n . 2
2 lssvancl.w . . . . . 6
3 lmodabl 15992 . . . . . 6
42, 3syl 16 . . . . 5
5 lssvancl.u . . . . . 6
6 lssvancl.x . . . . . 6
7 lssvancl.v . . . . . . 7
8 lssvancl.s . . . . . . 7
97, 8lssel 16015 . . . . . 6
105, 6, 9syl2anc 644 . . . . 5
11 lssvancl.y . . . . 5
12 lssvancl.p . . . . . 6
13 eqid 2437 . . . . . 6
147, 12, 13ablpncan2 15441 . . . . 5
154, 10, 11, 14syl3anc 1185 . . . 4