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

Theorem lspsnid 17771
Description: A vector belongs to the span of its singleton. (spansnid 26619 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
Hypotheses
Ref Expression
lspsnid.v  |-  V  =  ( Base `  W
)
lspsnid.n  |-  N  =  ( LSpan `  W )
Assertion
Ref Expression
lspsnid  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  X  e.  ( N `  { X } ) )

Proof of Theorem lspsnid
StepHypRef Expression
1 snssi 4101 . . 3  |-  ( X  e.  V  ->  { X }  C_  V )
2 lspsnid.v . . . 4  |-  V  =  ( Base `  W
)
3 lspsnid.n . . . 4  |-  N  =  ( LSpan `  W )
42, 3lspssid 17763 . . 3  |-  ( ( W  e.  LMod  /\  { X }  C_  V )  ->  { X }  C_  ( N `  { X } ) )
51, 4sylan2 472 . 2  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  { X }  C_  ( N `  { X } ) )
6 snssg 4090 . . 3  |-  ( X  e.  V  ->  ( X  e.  ( N `  { X } )  <->  { X }  C_  ( N `  { X } ) ) )
76adantl 464 . 2  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  ( X  e.  ( N `  { X } )  <->  { X }  C_  ( N `  { X } ) ) )
85, 7mpbird 232 1  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  X  e.  ( N `  { X } ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1399    e. wcel 1836    C_ wss 3402   {csn 3957   ` cfv 5509   Basecbs 14653   LModclmod 17644   LSpanclspn 17749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-rep 4491  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-reu 2749  df-rmo 2750  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-int 4213  df-iun 4258  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-riota 6176  df-ov 6217  df-0g 14868  df-mgm 16008  df-sgrp 16047  df-mnd 16057  df-grp 16193  df-lmod 17646  df-lss 17711  df-lsp 17750
This theorem is referenced by:  lspsnel6  17772  lssats2  17778  lspsneli  17779  lspsn  17780  lspsneq0  17790  lsmelval2  17863  lspprabs  17873  lspabs3  17899  lspsnel4  17902  lspdisjb  17904  lspfixed  17906  lshpnelb  35157  lsateln0  35168  lssats  35185  dia1dimid  37238  dochnel  37568  dihjat1lem  37603  dochsnkr2cl  37649  lcfrvalsnN  37716  lcfrlem15  37732  mapdpglem2  37848  mapdpglem9  37855  mapdpglem12  37858  mapdpglem14  37860  mapdindp0  37894  mapdindp3  37897  hdmap11lem2  38020  hdmaprnlem3N  38028  hdmaprnlem7N  38033  hdmaprnlem8N  38034  hdmaprnlem3eN  38036  hdmaplkr  38091
  Copyright terms: Public domain W3C validator