![]() |
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 2733 | . . 3 β’ (Scalarβπ) = (Scalarβπ) | |
2 | eqid 2733 | . . 3 β’ (Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) | |
3 | lssss.v | . . 3 β’ π = (Baseβπ) | |
4 | eqid 2733 | . . 3 β’ (+gβπ) = (+gβπ) | |
5 | eqid 2733 | . . 3 β’ ( Β·π βπ) = ( Β·π βπ) | |
6 | lssss.s | . . 3 β’ π = (LSubSpβπ) | |
7 | 1, 2, 3, 4, 5, 6 | islss 20410 | . 2 β’ (π β π β (π β π β§ π β β β§ βπ₯ β (Baseβ(Scalarβπ))βπ β π βπ β π ((π₯( Β·π βπ)π)(+gβπ)π) β π)) |
8 | 7 | simp1bi 1146 | 1 β’ (π β π β π β π) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 = wceq 1542 β wcel 2107 β wne 2940 βwral 3061 β wss 3911 β c0 4283 βcfv 6497 (class class class)co 7358 Basecbs 17088 +gcplusg 17138 Scalarcsca 17141 Β·π cvsca 17142 LSubSpclss 20407 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5257 ax-nul 5264 ax-pow 5321 ax-pr 5385 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-pw 4563 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-opab 5169 df-mpt 5190 df-id 5532 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-iota 6449 df-fun 6499 df-fv 6505 df-ov 7361 df-lss 20408 |
This theorem is referenced by: lssel 20413 lssuni 20415 00lss 20417 lsssubg 20433 islss3 20435 lsslss 20437 lssintcl 20440 lssmre 20442 lssacs 20443 lspid 20458 lspssv 20459 lspssp 20464 lsslsp 20491 lmhmima 20523 reslmhm 20528 lsmsp 20562 pj1lmhm 20576 lsppratlem2 20625 lsppratlem3 20626 lsppratlem4 20627 lspprat 20630 lbsextlem3 20637 lidlss 20696 ocvin 21094 pjdm2 21133 pjff 21134 pjf2 21136 pjfo 21137 pjcss 21138 frlmgsum 21194 frlmsplit2 21195 lsslindf 21252 lsslinds 21253 cphsscph 24631 lssbn 24732 minveclem1 24804 minveclem2 24806 minveclem3a 24807 minveclem3b 24808 minveclem3 24809 minveclem4a 24810 minveclem4b 24811 minveclem4 24812 minveclem6 24814 minveclem7 24815 pjthlem1 24817 pjthlem2 24818 pjth 24819 lssdimle 32360 ply1degltdimlem 32374 ply1degltdim 32375 islshpsm 37488 lshpnelb 37492 lshpnel2N 37493 lshpcmp 37496 lsatssv 37506 lssats 37520 lpssat 37521 lssatle 37523 lssat 37524 islshpcv 37561 lkrssv 37604 lkrlsp 37610 dvhopellsm 39626 dvadiaN 39637 dihss 39760 dihrnss 39787 dochord2N 39880 dochord3 39881 dihoml4 39886 dochsat 39892 dochshpncl 39893 dochnoncon 39900 djhlsmcl 39923 dihjat1lem 39937 dochsatshp 39960 dochsatshpb 39961 dochshpsat 39963 dochexmidlem2 39970 dochexmidlem5 39973 dochexmidlem6 39974 dochexmidlem7 39975 dochexmidlem8 39976 lclkrlem2p 40031 lclkrlem2v 40037 lcfrlem5 40055 lcfr 40094 mapdpglem17N 40197 mapdpglem18 40198 mapdpglem21 40201 islssfg 41440 islssfg2 41441 lnmlsslnm 41451 kercvrlsm 41453 lnmepi 41455 filnm 41460 gsumlsscl 46545 lincellss 46593 ellcoellss 46602 |
Copyright terms: Public domain | W3C validator |