![]() |
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 20889). (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 4813 | . 2 ⊢ (𝑋 ∈ 𝑉 → {𝑋} ⊆ 𝑉) | |
2 | lspval.v | . . 3 ⊢ 𝑉 = (Base‘𝑊) | |
3 | lspval.s | . . 3 ⊢ 𝑆 = (LSubSp‘𝑊) | |
4 | lspval.n | . . 3 ⊢ 𝑁 = (LSpan‘𝑊) | |
5 | 2, 3, 4 | lspcl 20889 | . 2 ⊢ ((𝑊 ∈ LMod ∧ {𝑋} ⊆ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆) |
6 | 1, 5 | sylan2 591 | 1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ∈ wcel 2098 ⊆ wss 3944 {csn 4630 ‘cfv 6549 Basecbs 17199 LModclmod 20772 LSubSpclss 20844 LSpanclspn 20884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 ax-un 7741 ax-cnex 11201 ax-resscn 11202 ax-1cn 11203 ax-icn 11204 ax-addcl 11205 ax-addrcl 11206 ax-mulcl 11207 ax-mulrcl 11208 ax-mulcom 11209 ax-addass 11210 ax-mulass 11211 ax-distr 11212 ax-i2m1 11213 ax-1ne0 11214 ax-1rid 11215 ax-rnegex 11216 ax-rrecex 11217 ax-cnre 11218 ax-pre-lttri 11219 ax-pre-lttrn 11220 ax-pre-ltadd 11221 ax-pre-mulgt0 11222 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3964 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-int 4951 df-iun 4999 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-pred 6307 df-ord 6374 df-on 6375 df-lim 6376 df-suc 6377 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-fo 6555 df-f1o 6556 df-fv 6557 df-riota 7375 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7872 df-1st 7994 df-2nd 7995 df-frecs 8287 df-wrecs 8318 df-recs 8392 df-rdg 8431 df-er 8725 df-en 8965 df-dom 8966 df-sdom 8967 df-pnf 11287 df-mnf 11288 df-xr 11289 df-ltxr 11290 df-le 11291 df-sub 11483 df-neg 11484 df-nn 12251 df-2 12313 df-sets 17152 df-slot 17170 df-ndx 17182 df-base 17200 df-plusg 17265 df-0g 17442 df-mgm 18619 df-sgrp 18698 df-mnd 18714 df-grp 18917 df-minusg 18918 df-sbg 18919 df-mgp 20104 df-ur 20151 df-ring 20204 df-lmod 20774 df-lss 20845 df-lsp 20885 |
This theorem is referenced by: lspsnsubg 20893 lspsneli 20914 lspsn 20915 lspsnss2 20918 lsmelval2 20999 lsmpr 21003 lsppr 21007 lspprabs 21009 lspsncmp 21033 lspsnne1 21034 lspsnne2 21035 lspabs3 21038 lspsneq 21039 lspdisj 21042 lspdisj2 21044 lspfixed 21045 lspexchn1 21047 lspindpi 21049 lsmcv 21058 lshpnel 38605 lshpnelb 38606 lshpnel2N 38607 lshpdisj 38609 lsatlss 38618 lsmsat 38630 lsatfixedN 38631 lssats 38634 lsmcv2 38651 lsat0cv 38655 lkrlsp 38724 lkrlsp3 38726 lshpsmreu 38731 lshpkrlem5 38736 dochnel 41016 djhlsmat 41050 dihjat1lem 41051 dvh3dim3N 41072 lclkrlem2b 41131 lclkrlem2f 41135 lclkrlem2p 41145 lcfrvalsnN 41164 lcfrlem23 41188 mapdsn 41264 mapdn0 41292 mapdncol 41293 mapdindp 41294 mapdpglem1 41295 mapdpglem2a 41297 mapdpglem3 41298 mapdpglem6 41301 mapdpglem8 41302 mapdpglem9 41303 mapdpglem12 41306 mapdpglem13 41307 mapdpglem14 41308 mapdpglem17N 41311 mapdpglem18 41312 mapdpglem19 41313 mapdpglem21 41315 mapdpglem23 41317 mapdpglem29 41323 mapdindp0 41342 mapdheq4lem 41354 mapdh6lem1N 41356 mapdh6lem2N 41357 mapdh6dN 41362 lspindp5 41393 hdmaplem3 41396 mapdh9a 41412 hdmap1l6lem1 41430 hdmap1l6lem2 41431 hdmap1l6d 41436 hdmap1eulem 41445 hdmap11lem2 41465 hdmapeq0 41467 hdmaprnlem1N 41472 hdmaprnlem3N 41473 hdmaprnlem3uN 41474 hdmaprnlem4N 41476 hdmaprnlem7N 41478 hdmaprnlem8N 41479 hdmaprnlem9N 41480 hdmaprnlem3eN 41481 hdmaprnlem16N 41485 hdmap14lem9 41499 hgmaprnlem2N 41520 hdmapglem7a 41550 |
Copyright terms: Public domain | W3C validator |