![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lspsncl | Structured version Visualization version GIF version |
Description: The span of a singleton is a subspace (frequently used special case of lspcl 19099). (Contributed by NM, 17-Jul-2014.) |
Ref | Expression |
---|---|
lspval.v | ⊢ 𝑉 = (Base‘𝑊) |
lspval.s | ⊢ 𝑆 = (LSubSp‘𝑊) |
lspval.n | ⊢ 𝑁 = (LSpan‘𝑊) |
Ref | Expression |
---|---|
lspsncl | ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snssi 4447 | . 2 ⊢ (𝑋 ∈ 𝑉 → {𝑋} ⊆ 𝑉) | |
2 | lspval.v | . . 3 ⊢ 𝑉 = (Base‘𝑊) | |
3 | lspval.s | . . 3 ⊢ 𝑆 = (LSubSp‘𝑊) | |
4 | lspval.n | . . 3 ⊢ 𝑁 = (LSpan‘𝑊) | |
5 | 2, 3, 4 | lspcl 19099 | . 2 ⊢ ((𝑊 ∈ LMod ∧ {𝑋} ⊆ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆) |
6 | 1, 5 | sylan2 492 | 1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1596 ∈ wcel 2103 ⊆ wss 3680 {csn 4285 ‘cfv 6001 Basecbs 15980 LModclmod 18986 LSubSpclss 19055 LSpanclspn 19094 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-8 2105 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-rep 4879 ax-sep 4889 ax-nul 4897 ax-pow 4948 ax-pr 5011 ax-un 7066 ax-cnex 10105 ax-resscn 10106 ax-1cn 10107 ax-icn 10108 ax-addcl 10109 ax-addrcl 10110 ax-mulcl 10111 ax-mulrcl 10112 ax-mulcom 10113 ax-addass 10114 ax-mulass 10115 ax-distr 10116 ax-i2m1 10117 ax-1ne0 10118 ax-1rid 10119 ax-rnegex 10120 ax-rrecex 10121 ax-cnre 10122 ax-pre-lttri 10123 ax-pre-lttrn 10124 ax-pre-ltadd 10125 ax-pre-mulgt0 10126 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ne 2897 df-nel 3000 df-ral 3019 df-rex 3020 df-reu 3021 df-rmo 3022 df-rab 3023 df-v 3306 df-sbc 3542 df-csb 3640 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-pss 3696 df-nul 4024 df-if 4195 df-pw 4268 df-sn 4286 df-pr 4288 df-tp 4290 df-op 4292 df-uni 4545 df-int 4584 df-iun 4630 df-br 4761 df-opab 4821 df-mpt 4838 df-tr 4861 df-id 5128 df-eprel 5133 df-po 5139 df-so 5140 df-fr 5177 df-we 5179 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 df-pred 5793 df-ord 5839 df-on 5840 df-lim 5841 df-suc 5842 df-iota 5964 df-fun 6003 df-fn 6004 df-f 6005 df-f1 6006 df-fo 6007 df-f1o 6008 df-fv 6009 df-riota 6726 df-ov 6768 df-oprab 6769 df-mpt2 6770 df-om 7183 df-1st 7285 df-2nd 7286 df-wrecs 7527 df-recs 7588 df-rdg 7626 df-er 7862 df-en 8073 df-dom 8074 df-sdom 8075 df-pnf 10189 df-mnf 10190 df-xr 10191 df-ltxr 10192 df-le 10193 df-sub 10381 df-neg 10382 df-nn 11134 df-2 11192 df-ndx 15983 df-slot 15984 df-base 15986 df-sets 15987 df-plusg 16077 df-0g 16225 df-mgm 17364 df-sgrp 17406 df-mnd 17417 df-grp 17547 df-minusg 17548 df-sbg 17549 df-mgp 18611 df-ur 18623 df-ring 18670 df-lmod 18988 df-lss 19056 df-lsp 19095 |
This theorem is referenced by: lspsnsubg 19103 lspsneli 19124 lspsn 19125 lspsnss2 19128 lsmelval2 19208 lsmpr 19212 lsppr 19216 lspprabs 19218 lspsncmp 19239 lspsnne1 19240 lspsnne2 19241 lspabs3 19244 lspsneq 19245 lspdisj 19248 lspdisj2 19250 lspfixed 19251 lspexchn1 19253 lspindpi 19255 lsmcv 19264 lshpnel 34690 lshpnelb 34691 lshpnel2N 34692 lshpdisj 34694 lsatlss 34703 lsmsat 34715 lsatfixedN 34716 lssats 34719 lsmcv2 34736 lsat0cv 34740 lkrlsp 34809 lkrlsp3 34811 lshpsmreu 34816 lshpkrlem5 34821 dochnel 37101 djhlsmat 37135 dihjat1lem 37136 dvh3dim3N 37157 lclkrlem2b 37216 lclkrlem2f 37220 lclkrlem2p 37230 lcfrvalsnN 37249 lcfrlem23 37273 mapdsn 37349 mapdn0 37377 mapdncol 37378 mapdindp 37379 mapdpglem1 37380 mapdpglem2a 37382 mapdpglem3 37383 mapdpglem6 37386 mapdpglem8 37387 mapdpglem9 37388 mapdpglem12 37391 mapdpglem13 37392 mapdpglem14 37393 mapdpglem17N 37396 mapdpglem18 37397 mapdpglem19 37398 mapdpglem21 37400 mapdpglem23 37402 mapdpglem29 37408 mapdindp0 37427 mapdheq4lem 37439 mapdh6lem1N 37441 mapdh6lem2N 37442 mapdh6dN 37447 lspindp5 37478 hdmaplem3 37481 mapdh9a 37498 hdmap1l6lem1 37516 hdmap1l6lem2 37517 hdmap1l6d 37522 hdmap1eulem 37532 hdmap11lem2 37553 hdmapeq0 37555 hdmaprnlem1N 37560 hdmaprnlem3N 37561 hdmaprnlem3uN 37562 hdmaprnlem4N 37564 hdmaprnlem7N 37566 hdmaprnlem8N 37567 hdmaprnlem9N 37568 hdmaprnlem3eN 37569 hdmaprnlem16N 37573 hdmap14lem9 37587 hgmaprnlem2N 37608 hdmapglem7a 37638 |
Copyright terms: Public domain | W3C validator |