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

Theorem lspdisjb 16190
 Description: A nonzero vector is not in a subspace iff its span is disjoint with the subspace. (Contributed by NM, 23-Apr-2015.)
Hypotheses
Ref Expression
lspdisjb.v
lspdisjb.o
lspdisjb.n
lspdisjb.s
lspdisjb.w
lspdisjb.u
lspdisjb.x
Assertion
Ref Expression
lspdisjb

Proof of Theorem lspdisjb
StepHypRef Expression
1 lspdisjb.v . . 3
2 lspdisjb.o . . 3
3 lspdisjb.n . . 3
4 lspdisjb.s . . 3
5 lspdisjb.w . . . 4
7 lspdisjb.u . . . 4
9 lspdisjb.x . . . . 5
109eldifad 3324 . . . 4
12 simpr 448 . . 3
131, 2, 3, 4, 6, 8, 11, 12lspdisj 16189 . 2
14 eldifsni 3920 . . . . 5
159, 14syl 16 . . . 4
17 lveclmod 16170 . . . . . . 7
185, 17syl 16 . . . . . 6
191, 3lspsnid 16061 . . . . . 6
2018, 10, 19syl2anc 643 . . . . 5
21 elin 3522 . . . . . . 7
22 eleq2 2496 . . . . . . . 8
23 elsni 3830 . . . . . . . 8
2422, 23syl6bi 220 . . . . . . 7
2521, 24syl5bir 210 . . . . . 6
2625exp3a 426 . . . . 5
2720, 26mpan9 456 . . . 4