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

Theorem lspsnel4 16196
 Description: A member of the span of the singleton of a vector is a member of a subspace containing the vector. (elspansn4 23075 analog.) (Contributed by NM, 4-Jul-2014.)
Hypotheses
Ref Expression
lspsnel4.v
lspsnel4.o
lspsnel4.s
lspsnel4.n
lspsnel4.w
lspsnel4.u
lspsnel4.x
lspsnel4.y
lspsnel4.z
Assertion
Ref Expression
lspsnel4

Proof of Theorem lspsnel4
StepHypRef Expression
1 lspsnel4.s . . 3
2 lspsnel4.n . . 3
3 lspsnel4.w . . . . 5
4 lveclmod 16178 . . . . 5
53, 4syl 16 . . . 4
7 lspsnel4.u . . . 4
9 simpr 448 . . 3
10 lspsnel4.y . . . 4
121, 2, 6, 8, 9, 11lspsnel3 16067 . 2
15 simpr 448 . . 3
16 lspsnel4.x . . . . . 6
17 lspsnel4.v . . . . . . 7
1817, 2lspsnid 16069 . . . . . 6
195, 16, 18syl2anc 643 . . . . 5
20 lspsnel4.o . . . . . 6
21 lspsnel4.z . . . . . 6
2217, 20, 2, 3, 16, 10, 21lspsneleq 16187 . . . . 5
2319, 22eleqtrrd 2513 . . . 4