Theorem lspsncl 20311

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540   ∈ wcel 2105   ⊆ wss 3897  {csn 4571  ‘cfv 6465  Basecbs 16982  LModclmod 20195  LSubSpclss 20265  LSpanclspn 20305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-cnex 11000  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020  ax-pre-mulgt0 11021

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-riota 7272  df-ov 7318  df-oprab 7319  df-mpo 7320  df-om 7758  df-1st 7876  df-2nd 7877  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-er 8546  df-en 8782  df-dom 8783  df-sdom 8784  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-sub 11280  df-neg 11281  df-nn 12047  df-2 12109  df-sets 16935  df-slot 16953  df-ndx 16965  df-base 16983  df-plusg 17045  df-0g 17222  df-mgm 18396  df-sgrp 18445  df-mnd 18456  df-grp 18649  df-minusg 18650  df-sbg 18651  df-mgp 19789  df-ur 19806  df-ring 19853  df-lmod 20197  df-lss 20266  df-lsp 20306

This theorem is referenced by:  lspsnsubg  20314  lspsneli  20335  lspsn  20336  lspsnss2  20339  lsmelval2  20419  lsmpr  20423  lsppr  20427  lspprabs  20429  lspsncmp  20450  lspsnne1  20451  lspsnne2  20452  lspabs3  20455  lspsneq  20456  lspdisj  20459  lspdisj2  20461  lspfixed  20462  lspexchn1  20464  lspindpi  20466  lsmcv  20475  lshpnel  37201  lshpnelb  37202  lshpnel2N  37203  lshpdisj  37205  lsatlss  37214  lsmsat  37226  lsatfixedN  37227  lssats  37230  lsmcv2  37247  lsat0cv  37251  lkrlsp  37320  lkrlsp3  37322  lshpsmreu  37327  lshpkrlem5  37332  dochnel  39612  djhlsmat  39646  dihjat1lem  39647  dvh3dim3N  39668  lclkrlem2b  39727  lclkrlem2f  39731  lclkrlem2p  39741  lcfrvalsnN  39760  lcfrlem23  39784  mapdsn  39860  mapdn0  39888  mapdncol  39889  mapdindp  39890  mapdpglem1  39891  mapdpglem2a  39893  mapdpglem3  39894  mapdpglem6  39897  mapdpglem8  39898  mapdpglem9  39899  mapdpglem12  39902  mapdpglem13  39903  mapdpglem14  39904  mapdpglem17N  39907  mapdpglem18  39908  mapdpglem19  39909  mapdpglem21  39911  mapdpglem23  39913  mapdpglem29  39919  mapdindp0  39938  mapdheq4lem  39950  mapdh6lem1N  39952  mapdh6lem2N  39953  mapdh6dN  39958  lspindp5  39989  hdmaplem3  39992  mapdh9a  40008  hdmap1l6lem1  40026  hdmap1l6lem2  40027  hdmap1l6d  40032  hdmap1eulem  40041  hdmap11lem2  40061  hdmapeq0  40063  hdmaprnlem1N  40068  hdmaprnlem3N  40069  hdmaprnlem3uN  40070  hdmaprnlem4N  40072  hdmaprnlem7N  40074  hdmaprnlem8N  40075  hdmaprnlem9N  40076  hdmaprnlem3eN  40077  hdmaprnlem16N  40081  hdmap14lem9  40095  hgmaprnlem2N  40116  hdmapglem7a  40146