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

Theorem lssss 18704
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 2609 . . 3 (Scalar‘𝑊) = (Scalar‘𝑊)
2 eqid 2609 . . 3 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
3 lssss.v . . 3 𝑉 = (Base‘𝑊)
4 eqid 2609 . . 3 (+g𝑊) = (+g𝑊)
5 eqid 2609 . . 3 ( ·𝑠𝑊) = ( ·𝑠𝑊)
6 lssss.s . . 3 𝑆 = (LSubSp‘𝑊)
71, 2, 3, 4, 5, 6islss 18702 . 2 (𝑈𝑆 ↔ (𝑈𝑉𝑈 ≠ ∅ ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑎𝑈𝑏𝑈 ((𝑥( ·𝑠𝑊)𝑎)(+g𝑊)𝑏) ∈ 𝑈))
87simp1bi 1068 1 (𝑈𝑆𝑈𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  wne 2779  wral 2895  wss 3539  c0 3873  cfv 5790  (class class class)co 6527  Basecbs 15641  +gcplusg 15714  Scalarcsca 15717   ·𝑠 cvsca 15718  LSubSpclss 18699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-iota 5754  df-fun 5792  df-fv 5798  df-ov 6530  df-lss 18700
This theorem is referenced by:  lssel  18705  lssuni  18707  00lss  18709  lsssubg  18724  islss3  18726  lsslss  18728  lssintcl  18731  lssmre  18733  lssacs  18734  lspid  18749  lspssv  18750  lspssp  18755  lsslsp  18782  lmhmima  18814  reslmhm  18819  lsmsp  18853  pj1lmhm  18867  lsppratlem2  18915  lsppratlem3  18916  lsppratlem4  18917  lspprat  18920  lbsextlem3  18927  lidlss  18977  ocvin  19779  pjdm2  19816  pjff  19817  pjf2  19819  pjfo  19820  pjcss  19821  frlmgsum  19872  frlmsplit2  19873  lsslindf  19930  lsslinds  19931  lssbn  22873  minveclem1  22920  minveclem2  22922  minveclem3a  22923  minveclem3b  22924  minveclem3  22925  minveclem4a  22926  minveclem4b  22927  minveclem4  22928  minveclem6  22930  minveclem7  22931  pjthlem1  22933  pjthlem2  22934  pjth  22935  islshpsm  33081  lshpnelb  33085  lshpnel2N  33086  lshpcmp  33089  lsatssv  33099  lssats  33113  lpssat  33114  lssatle  33116  lssat  33117  islshpcv  33154  lkrssv  33197  lkrlsp  33203  dvhopellsm  35220  dvadiaN  35231  dihss  35354  dihrnss  35381  dochord2N  35474  dochord3  35475  dihoml4  35480  dochsat  35486  dochshpncl  35487  dochnoncon  35494  djhlsmcl  35517  dihjat1lem  35531  dochsatshp  35554  dochsatshpb  35555  dochshpsat  35557  dochexmidlem2  35564  dochexmidlem5  35567  dochexmidlem6  35568  dochexmidlem7  35569  dochexmidlem8  35570  lclkrlem2p  35625  lclkrlem2v  35631  lcfrlem5  35649  lcfr  35688  mapdpglem17N  35791  mapdpglem18  35792  mapdpglem21  35795  islssfg  36454  islssfg2  36455  lnmlsslnm  36465  kercvrlsm  36467  lnmepi  36469  filnm  36474  gsumlsscl  41953  lincellss  42004  ellcoellss  42013
  Copyright terms: Public domain W3C validator