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

Theorem lssss 19700
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 2819 . . 3 (Scalar‘𝑊) = (Scalar‘𝑊)
2 eqid 2819 . . 3 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
3 lssss.v . . 3 𝑉 = (Base‘𝑊)
4 eqid 2819 . . 3 (+g𝑊) = (+g𝑊)
5 eqid 2819 . . 3 ( ·𝑠𝑊) = ( ·𝑠𝑊)
6 lssss.s . . 3 𝑆 = (LSubSp‘𝑊)
71, 2, 3, 4, 5, 6islss 19698 . 2 (𝑈𝑆 ↔ (𝑈𝑉𝑈 ≠ ∅ ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑎𝑈𝑏𝑈 ((𝑥( ·𝑠𝑊)𝑎)(+g𝑊)𝑏) ∈ 𝑈))
87simp1bi 1140 1 (𝑈𝑆𝑈𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1531  wcel 2108  wne 3014  wral 3136  wss 3934  c0 4289  cfv 6348  (class class class)co 7148  Basecbs 16475  +gcplusg 16557  Scalarcsca 16560   ·𝑠 cvsca 16561  LSubSpclss 19695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fv 6356  df-ov 7151  df-lss 19696
This theorem is referenced by:  lssel  19701  lssuni  19703  00lss  19705  lsssubg  19721  islss3  19723  lsslss  19725  lssintcl  19728  lssmre  19730  lssacs  19731  lspid  19746  lspssv  19747  lspssp  19752  lsslsp  19779  lmhmima  19811  reslmhm  19816  lsmsp  19850  pj1lmhm  19864  lsppratlem2  19912  lsppratlem3  19913  lsppratlem4  19914  lspprat  19917  lbsextlem3  19924  lidlss  19975  ocvin  20810  pjdm2  20847  pjff  20848  pjf2  20850  pjfo  20851  pjcss  20852  frlmgsum  20908  frlmsplit2  20909  lsslindf  20966  lsslinds  20967  cphsscph  23846  lssbn  23947  minveclem1  24019  minveclem2  24021  minveclem3a  24022  minveclem3b  24023  minveclem3  24024  minveclem4a  24025  minveclem4b  24026  minveclem4  24027  minveclem6  24029  minveclem7  24030  pjthlem1  24032  pjthlem2  24033  pjth  24034  lssdimle  30999  islshpsm  36108  lshpnelb  36112  lshpnel2N  36113  lshpcmp  36116  lsatssv  36126  lssats  36140  lpssat  36141  lssatle  36143  lssat  36144  islshpcv  36181  lkrssv  36224  lkrlsp  36230  dvhopellsm  38245  dvadiaN  38256  dihss  38379  dihrnss  38406  dochord2N  38499  dochord3  38500  dihoml4  38505  dochsat  38511  dochshpncl  38512  dochnoncon  38519  djhlsmcl  38542  dihjat1lem  38556  dochsatshp  38579  dochsatshpb  38580  dochshpsat  38582  dochexmidlem2  38589  dochexmidlem5  38592  dochexmidlem6  38593  dochexmidlem7  38594  dochexmidlem8  38595  lclkrlem2p  38650  lclkrlem2v  38656  lcfrlem5  38674  lcfr  38713  mapdpglem17N  38816  mapdpglem18  38817  mapdpglem21  38820  islssfg  39661  islssfg2  39662  lnmlsslnm  39672  kercvrlsm  39674  lnmepi  39676  filnm  39681  gsumlsscl  44422  lincellss  44472  ellcoellss  44481
  Copyright terms: Public domain W3C validator