![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lssss | Structured version Visualization version GIF version |
Description: A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.) |
Ref | Expression |
---|---|
lssss.v | ⊢ 𝑉 = (Base‘𝑊) |
lssss.s | ⊢ 𝑆 = (LSubSp‘𝑊) |
Ref | Expression |
---|---|
lssss | ⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2798 | . . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
2 | eqid 2798 | . . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | |
3 | lssss.v | . . 3 ⊢ 𝑉 = (Base‘𝑊) | |
4 | eqid 2798 | . . 3 ⊢ (+g‘𝑊) = (+g‘𝑊) | |
5 | eqid 2798 | . . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊) | |
6 | lssss.s | . . 3 ⊢ 𝑆 = (LSubSp‘𝑊) | |
7 | 1, 2, 3, 4, 5, 6 | islss 19699 | . 2 ⊢ (𝑈 ∈ 𝑆 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥( ·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑈)) |
8 | 7 | simp1bi 1142 | 1 ⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 ∈ wcel 2111 ≠ wne 2987 ∀wral 3106 ⊆ wss 3881 ∅c0 4243 ‘cfv 6324 (class class class)co 7135 Basecbs 16475 +gcplusg 16557 Scalarcsca 16560 ·𝑠 cvsca 16561 LSubSpclss 19696 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-iota 6283 df-fun 6326 df-fv 6332 df-ov 7138 df-lss 19697 |
This theorem is referenced by: lssel 19702 lssuni 19704 00lss 19706 lsssubg 19722 islss3 19724 lsslss 19726 lssintcl 19729 lssmre 19731 lssacs 19732 lspid 19747 lspssv 19748 lspssp 19753 lsslsp 19780 lmhmima 19812 reslmhm 19817 lsmsp 19851 pj1lmhm 19865 lsppratlem2 19913 lsppratlem3 19914 lsppratlem4 19915 lspprat 19918 lbsextlem3 19925 lidlss 19976 ocvin 20363 pjdm2 20400 pjff 20401 pjf2 20403 pjfo 20404 pjcss 20405 frlmgsum 20461 frlmsplit2 20462 lsslindf 20519 lsslinds 20520 cphsscph 23855 lssbn 23956 minveclem1 24028 minveclem2 24030 minveclem3a 24031 minveclem3b 24032 minveclem3 24033 minveclem4a 24034 minveclem4b 24035 minveclem4 24036 minveclem6 24038 minveclem7 24039 pjthlem1 24041 pjthlem2 24042 pjth 24043 lssdimle 31094 islshpsm 36276 lshpnelb 36280 lshpnel2N 36281 lshpcmp 36284 lsatssv 36294 lssats 36308 lpssat 36309 lssatle 36311 lssat 36312 islshpcv 36349 lkrssv 36392 lkrlsp 36398 dvhopellsm 38413 dvadiaN 38424 dihss 38547 dihrnss 38574 dochord2N 38667 dochord3 38668 dihoml4 38673 dochsat 38679 dochshpncl 38680 dochnoncon 38687 djhlsmcl 38710 dihjat1lem 38724 dochsatshp 38747 dochsatshpb 38748 dochshpsat 38750 dochexmidlem2 38757 dochexmidlem5 38760 dochexmidlem6 38761 dochexmidlem7 38762 dochexmidlem8 38763 lclkrlem2p 38818 lclkrlem2v 38824 lcfrlem5 38842 lcfr 38881 mapdpglem17N 38984 mapdpglem18 38985 mapdpglem21 38988 islssfg 40014 islssfg2 40015 lnmlsslnm 40025 kercvrlsm 40027 lnmepi 40029 filnm 40034 gsumlsscl 44785 lincellss 44835 ellcoellss 44844 |
Copyright terms: Public domain | W3C validator |