MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lssss Structured version   Visualization version   GIF version

Theorem lssss 20412
Description: A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
Hypotheses
Ref Expression
lssss.v 𝑉 = (Baseβ€˜π‘Š)
lssss.s 𝑆 = (LSubSpβ€˜π‘Š)
Assertion
Ref Expression
lssss (π‘ˆ ∈ 𝑆 β†’ π‘ˆ βŠ† 𝑉)

Proof of Theorem lssss
Dummy variables π‘Ž 𝑏 π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef 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β€˜π‘Š)
71, 2, 3, 4, 5, 6islss 20410 . 2 (π‘ˆ ∈ 𝑆 ↔ (π‘ˆ βŠ† 𝑉 ∧ π‘ˆ β‰  βˆ… ∧ βˆ€π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘Ž ∈ π‘ˆ βˆ€π‘ ∈ π‘ˆ ((π‘₯( ·𝑠 β€˜π‘Š)π‘Ž)(+gβ€˜π‘Š)𝑏) ∈ π‘ˆ))
87simp1bi 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