Theorem lspsncl 20154

Description: The span of a singleton is a subspace (frequently used special case of lspcl 20153). (Contributed by NM, 17-Jul-2014.)

Hypotheses

Ref	Expression
lspval.v	⊢ 𝑉 = (Base‘𝑊)
lspval.s	⊢ 𝑆 = (LSubSp‘𝑊)
lspval.n	⊢ 𝑁 = (LSpan‘𝑊)

Assertion

Ref	Expression
lspsncl	⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆)

Proof of Theorem lspsncl

Step	Hyp	Ref	Expression
1		snssi 4738	. 2 ⊢ (𝑋 ∈ 𝑉 → {𝑋} ⊆ 𝑉)
2		lspval.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
3		lspval.s	. . 3 ⊢ 𝑆 = (LSubSp‘𝑊)
4		lspval.n	. . 3 ⊢ 𝑁 = (LSpan‘𝑊)
5	2, 3, 4	lspcl 20153	. 2 ⊢ ((𝑊 ∈ LMod ∧ {𝑋} ⊆ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆)
6	1, 5	sylan2 592	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108   ⊆ wss 3883  {csn 4558  ‘cfv 6418  Basecbs 16840  LModclmod 20038  LSubSpclss 20108  LSpanclspn 20148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904  df-2 11966  df-sets 16793  df-slot 16811  df-ndx 16823  df-base 16841  df-plusg 16901  df-0g 17069  df-mgm 18241  df-sgrp 18290  df-mnd 18301  df-grp 18495  df-minusg 18496  df-sbg 18497  df-mgp 19636  df-ur 19653  df-ring 19700  df-lmod 20040  df-lss 20109  df-lsp 20149

This theorem is referenced by:  lspsnsubg  20157  lspsneli  20178  lspsn  20179  lspsnss2  20182  lsmelval2  20262  lsmpr  20266  lsppr  20270  lspprabs  20272  lspsncmp  20293  lspsnne1  20294  lspsnne2  20295  lspabs3  20298  lspsneq  20299  lspdisj  20302  lspdisj2  20304  lspfixed  20305  lspexchn1  20307  lspindpi  20309  lsmcv  20318  lshpnel  36924  lshpnelb  36925  lshpnel2N  36926  lshpdisj  36928  lsatlss  36937  lsmsat  36949  lsatfixedN  36950  lssats  36953  lsmcv2  36970  lsat0cv  36974  lkrlsp  37043  lkrlsp3  37045  lshpsmreu  37050  lshpkrlem5  37055  dochnel  39334  djhlsmat  39368  dihjat1lem  39369  dvh3dim3N  39390  lclkrlem2b  39449  lclkrlem2f  39453  lclkrlem2p  39463  lcfrvalsnN  39482  lcfrlem23  39506  mapdsn  39582  mapdn0  39610  mapdncol  39611  mapdindp  39612  mapdpglem1  39613  mapdpglem2a  39615  mapdpglem3  39616  mapdpglem6  39619  mapdpglem8  39620  mapdpglem9  39621  mapdpglem12  39624  mapdpglem13  39625  mapdpglem14  39626  mapdpglem17N  39629  mapdpglem18  39630  mapdpglem19  39631  mapdpglem21  39633  mapdpglem23  39635  mapdpglem29  39641  mapdindp0  39660  mapdheq4lem  39672  mapdh6lem1N  39674  mapdh6lem2N  39675  mapdh6dN  39680  lspindp5  39711  hdmaplem3  39714  mapdh9a  39730  hdmap1l6lem1  39748  hdmap1l6lem2  39749  hdmap1l6d  39754  hdmap1eulem  39763  hdmap11lem2  39783  hdmapeq0  39785  hdmaprnlem1N  39790  hdmaprnlem3N  39791  hdmaprnlem3uN  39792  hdmaprnlem4N  39794  hdmaprnlem7N  39796  hdmaprnlem8N  39797  hdmaprnlem9N  39798  hdmaprnlem3eN  39799  hdmaprnlem16N  39803  hdmap14lem9  39817  hgmaprnlem2N  39838  hdmapglem7a  39868