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 2821 | . . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
2 | eqid 2821 | . . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | |
3 | lssss.v | . . 3 ⊢ 𝑉 = (Base‘𝑊) | |
4 | eqid 2821 | . . 3 ⊢ (+g‘𝑊) = (+g‘𝑊) | |
5 | eqid 2821 | . . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊) | |
6 | lssss.s | . . 3 ⊢ 𝑆 = (LSubSp‘𝑊) | |
7 | 1, 2, 3, 4, 5, 6 | islss 19700 | . 2 ⊢ (𝑈 ∈ 𝑆 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥( ·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑈)) |
8 | 7 | simp1bi 1141 | 1 ⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2110 ≠ wne 3016 ∀wral 3138 ⊆ wss 3935 ∅c0 4290 ‘cfv 6349 (class class class)co 7150 Basecbs 16477 +gcplusg 16559 Scalarcsca 16562 ·𝑠 cvsca 16563 LSubSpclss 19697 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-op 4567 df-uni 4832 df-br 5059 df-opab 5121 df-mpt 5139 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-iota 6308 df-fun 6351 df-fv 6357 df-ov 7153 df-lss 19698 |
This theorem is referenced by: lssel 19703 lssuni 19705 00lss 19707 lsssubg 19723 islss3 19725 lsslss 19727 lssintcl 19730 lssmre 19732 lssacs 19733 lspid 19748 lspssv 19749 lspssp 19754 lsslsp 19781 lmhmima 19813 reslmhm 19818 lsmsp 19852 pj1lmhm 19866 lsppratlem2 19914 lsppratlem3 19915 lsppratlem4 19916 lspprat 19919 lbsextlem3 19926 lidlss 19977 ocvin 20812 pjdm2 20849 pjff 20850 pjf2 20852 pjfo 20853 pjcss 20854 frlmgsum 20910 frlmsplit2 20911 lsslindf 20968 lsslinds 20969 cphsscph 23848 lssbn 23949 minveclem1 24021 minveclem2 24023 minveclem3a 24024 minveclem3b 24025 minveclem3 24026 minveclem4a 24027 minveclem4b 24028 minveclem4 24029 minveclem6 24031 minveclem7 24032 pjthlem1 24034 pjthlem2 24035 pjth 24036 lssdimle 31001 islshpsm 36110 lshpnelb 36114 lshpnel2N 36115 lshpcmp 36118 lsatssv 36128 lssats 36142 lpssat 36143 lssatle 36145 lssat 36146 islshpcv 36183 lkrssv 36226 lkrlsp 36232 dvhopellsm 38247 dvadiaN 38258 dihss 38381 dihrnss 38408 dochord2N 38501 dochord3 38502 dihoml4 38507 dochsat 38513 dochshpncl 38514 dochnoncon 38521 djhlsmcl 38544 dihjat1lem 38558 dochsatshp 38581 dochsatshpb 38582 dochshpsat 38584 dochexmidlem2 38591 dochexmidlem5 38594 dochexmidlem6 38595 dochexmidlem7 38596 dochexmidlem8 38597 lclkrlem2p 38652 lclkrlem2v 38658 lcfrlem5 38676 lcfr 38715 mapdpglem17N 38818 mapdpglem18 38819 mapdpglem21 38822 islssfg 39663 islssfg2 39664 lnmlsslnm 39674 kercvrlsm 39676 lnmepi 39678 filnm 39683 gsumlsscl 44425 lincellss 44475 ellcoellss 44484 |
Copyright terms: Public domain | W3C validator |