Theorem lspsncl 21013

Description: The span of a singleton is a subspace (frequently used special case of lspcl 21012). (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 4734	. 2 ⊢ (𝑋 ∈ 𝑉 → {𝑋} ⊆ 𝑉)
2		lspval.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
3		lspval.s	. . 3 ⊢ 𝑆 = (LSubSp‘𝑊)
4		lspval.n	. . 3 ⊢ 𝑁 = (LSpan‘𝑊)
5	2, 3, 4	lspcl 21012	. 2 ⊢ ((𝑊 ∈ LMod ∧ {𝑋} ⊆ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆)
6	1, 5	sylan2 601	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1550   ∈ wcel 2132   ⊆ wss 3895  {csn 4572  ‘cfv 6506  Basecbs 17217  LModclmod 20896  LSubSpclss 20967  LSpanclspn 21007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-rep 5217  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-nel 3052  df-ral 3067  df-rex 3077  df-rmo 3357  df-reu 3358  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-pss 3915  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-int 4896  df-iun 4941  df-br 5091  df-opab 5153  df-mpt 5172  df-tr 5198  df-id 5531  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5589  df-we 5591  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-pred 6273  df-ord 6334  df-on 6335  df-lim 6336  df-suc 6337  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-riota 7338  df-ov 7384  df-oprab 7385  df-mpo 7386  df-om 7832  df-1st 7955  df-2nd 7956  df-frecs 8246  df-wrecs 8277  df-recs 8326  df-rdg 8365  df-er 8662  df-en 8913  df-dom 8914  df-sdom 8915  df-pnf 11204  df-mnf 11205  df-xr 11206  df-ltxr 11207  df-le 11208  df-sub 11402  df-neg 11403  df-nn 12197  df-2 12266  df-sets 17172  df-slot 17190  df-ndx 17202  df-base 17218  df-plusg 17271  df-0g 17442  df-mgm 18646  df-sgrp 18725  df-mnd 18741  df-grp 18950  df-minusg 18951  df-sbg 18952  df-mgp 20159  df-ur 20200  df-ring 20253  df-lmod 20898  df-lss 20968  df-lsp 21008

This theorem is referenced by:  lspsnsubg  21016  ellspsni  21037  lspsn  21038  lspsnss2  21041  lsmelval2  21121  lsmpr  21125  lsppr  21129  lspprabs  21131  lspsncmp  21155  lspsnne1  21156  lspsnne2  21157  lspabs3  21160  lspsneq  21161  lspdisj  21164  lspdisj2  21166  lspfixed  21167  lspexchn1  21169  lspindpi  21171  lsmcv  21180  lshpnel  39545  lshpnelb  39546  lshpnel2N  39547  lshpdisj  39549  lsatlss  39558  lsmsat  39570  lsatfixedN  39571  lssats  39574  lsmcv2  39591  lsat0cv  39595  lkrlsp  39664  lkrlsp3  39666  lshpsmreu  39671  lshpkrlem5  39676  dochnel  41955  djhlsmat  41989  dihjat1lem  41990  dvh3dim3N  42011  lclkrlem2b  42070  lclkrlem2f  42074  lclkrlem2p  42084  lcfrvalsnN  42103  lcfrlem23  42127  mapdsn  42203  mapdn0  42231  mapdncol  42232  mapdindp  42233  mapdpglem1  42234  mapdpglem2a  42236  mapdpglem3  42237  mapdpglem6  42240  mapdpglem8  42241  mapdpglem9  42242  mapdpglem12  42245  mapdpglem13  42246  mapdpglem14  42247  mapdpglem17N  42250  mapdpglem18  42251  mapdpglem19  42252  mapdpglem21  42254  mapdpglem23  42256  mapdpglem29  42262  mapdindp0  42281  mapdheq4lem  42293  mapdh6lem1N  42295  mapdh6lem2N  42296  mapdh6dN  42301  lspindp5  42332  hdmaplem3  42335  mapdh9a  42351  hdmap1l6lem1  42369  hdmap1l6lem2  42370  hdmap1l6d  42375  hdmap1eulem  42384  hdmap11lem2  42404  hdmapeq0  42406  hdmaprnlem1N  42411  hdmaprnlem3N  42412  hdmaprnlem3uN  42413  hdmaprnlem4N  42415  hdmaprnlem7N  42417  hdmaprnlem8N  42418  hdmaprnlem9N  42419  hdmaprnlem3eN  42420  hdmaprnlem16N  42424  hdmap14lem9  42438  hgmaprnlem2N  42459  hdmapglem7a  42489