MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lspsnel5a Structured version   Visualization version   GIF version

Theorem lspsnel5a 20409
Description: Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 20-Feb-2015.)
Hypotheses
Ref Expression
lspsnel5a.s 𝑆 = (LSubSp‘𝑊)
lspsnel5a.n 𝑁 = (LSpan‘𝑊)
lspsnel5a.w (𝜑𝑊 ∈ LMod)
lspsnel5a.a (𝜑𝑈𝑆)
lspsnel5a.x (𝜑𝑋𝑈)
Assertion
Ref Expression
lspsnel5a (𝜑 → (𝑁‘{𝑋}) ⊆ 𝑈)

Proof of Theorem lspsnel5a
StepHypRef Expression
1 lspsnel5a.x . 2 (𝜑𝑋𝑈)
2 eqid 2737 . . 3 (Base‘𝑊) = (Base‘𝑊)
3 lspsnel5a.s . . 3 𝑆 = (LSubSp‘𝑊)
4 lspsnel5a.n . . 3 𝑁 = (LSpan‘𝑊)
5 lspsnel5a.w . . 3 (𝜑𝑊 ∈ LMod)
6 lspsnel5a.a . . 3 (𝜑𝑈𝑆)
72, 3lssel 20350 . . . 4 ((𝑈𝑆𝑋𝑈) → 𝑋 ∈ (Base‘𝑊))
86, 1, 7syl2anc 584 . . 3 (𝜑𝑋 ∈ (Base‘𝑊))
92, 3, 4, 5, 6, 8lspsnel5 20408 . 2 (𝜑 → (𝑋𝑈 ↔ (𝑁‘{𝑋}) ⊆ 𝑈))
101, 9mpbid 231 1 (𝜑 → (𝑁‘{𝑋}) ⊆ 𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2106  wss 3908  {csn 4584  cfv 6493  Basecbs 17042  LModclmod 20274  LSubSpclss 20344  LSpanclspn 20384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-id 5529  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7307  df-ov 7354  df-0g 17282  df-mgm 18456  df-sgrp 18505  df-mnd 18516  df-grp 18710  df-lmod 20276  df-lss 20345  df-lsp 20385
This theorem is referenced by:  lssats2  20413  lspsn  20415  lspsnvsi  20417  lsmelval2  20498  lspprabs  20508  lspvadd  20509  lspabs3  20534  lsmcv  20554  lspsnat  20558  lsppratlem6  20565  issubassa2  21247  lshpnel  37376  lsatel  37398  lsmsat  37401  lssatomic  37404  lssats  37405  lsat0cv  37426  dia2dimlem10  39467  dochsatshpb  39846  lclkrlem2f  39906  lcfrlem25  39961  lcfrlem35  39971  mapdval2N  40024  mapdrvallem2  40039  mapdpglem8  40073  mapdpglem13  40078  mapdindp0  40113  mapdh6aN  40129  mapdh8e  40178  mapdh9a  40183  hdmap1l6a  40203  hdmapval0  40227  hdmapval3lemN  40231  hdmap10lem  40233  hdmap11lem1  40235  hdmap11lem2  40236  hdmaprnlem4N  40247  hdmaprnlem3eN  40252
  Copyright terms: Public domain W3C validator