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

Theorem lssss 18148
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  |-  V  =  ( Base `  W
)
lssss.s  |-  S  =  ( LSubSp `  W )
Assertion
Ref Expression
lssss  |-  ( U  e.  S  ->  U  C_  V )

Proof of Theorem lssss
Dummy variables  a 
b  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2422 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
2 eqid 2422 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
3 lssss.v . . 3  |-  V  =  ( Base `  W
)
4 eqid 2422 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
5 eqid 2422 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
6 lssss.s . . 3  |-  S  =  ( LSubSp `  W )
71, 2, 3, 4, 5, 6islss 18146 . 2  |-  ( U  e.  S  <->  ( U  C_  V  /\  U  =/=  (/)  /\  A. x  e.  ( Base `  (Scalar `  W ) ) A. a  e.  U  A. b  e.  U  (
( x ( .s
`  W ) a ) ( +g  `  W
) b )  e.  U ) )
87simp1bi 1020 1  |-  ( U  e.  S  ->  U  C_  V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1868    =/= wne 2618   A.wral 2775    C_ wss 3436   (/)c0 3761   ` cfv 5598  (class class class)co 6302   Basecbs 15109   +g cplusg 15178  Scalarcsca 15181   .scvsca 15182   LSubSpclss 18143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-iota 5562  df-fun 5600  df-fv 5606  df-ov 6305  df-lss 18144
This theorem is referenced by:  lssel  18149  lssuni  18151  00lss  18153  lsssubg  18168  islss3  18170  lsslss  18172  lssintcl  18175  lssmre  18177  lssacs  18178  lspid  18193  lspssv  18194  lspssp  18199  lsslsp  18226  lmhmima  18258  reslmhm  18263  lsmsp  18297  pj1lmhm  18311  lsppratlem2  18359  lsppratlem3  18360  lsppratlem4  18361  lspprat  18364  lbsextlem3  18371  lidlss  18421  ocvin  19224  pjdm2  19261  pjff  19262  pjf2  19264  pjfo  19265  pjcss  19266  frlmgsum  19317  frlmsplit2  19318  lsslindf  19375  lsslinds  19376  lssbn  22306  minveclem1  22353  minveclem2  22355  minveclem3a  22356  minveclem3b  22357  minveclem3  22358  minveclem4a  22359  minveclem4b  22360  minveclem4  22361  minveclem6  22363  minveclem7  22364  minveclem2OLD  22367  minveclem3aOLD  22368  minveclem3bOLD  22369  minveclem3OLD  22370  minveclem4aOLD  22371  minveclem4bOLD  22372  minveclem4OLD  22373  minveclem6OLD  22375  minveclem7OLD  22376  pjthlem1  22378  pjthlem2  22379  pjth  22380  islshpsm  32465  lshpnelb  32469  lshpnel2N  32470  lshpcmp  32473  lsatssv  32483  lssats  32497  lpssat  32498  lssatle  32500  lssat  32501  islshpcv  32538  lkrssv  32581  lkrlsp  32587  dvhopellsm  34604  dvadiaN  34615  dihss  34738  dihrnss  34765  dochord2N  34858  dochord3  34859  dihoml4  34864  dochsat  34870  dochshpncl  34871  dochnoncon  34878  djhlsmcl  34901  dihjat1lem  34915  dochsatshp  34938  dochsatshpb  34939  dochshpsat  34941  dochexmidlem2  34948  dochexmidlem5  34951  dochexmidlem6  34952  dochexmidlem7  34953  dochexmidlem8  34954  lclkrlem2p  35009  lclkrlem2v  35015  lcfrlem5  35033  lcfr  35072  mapdpglem17N  35175  mapdpglem18  35176  mapdpglem21  35179  islssfg  35848  islssfg2  35849  lnmlsslnm  35859  kercvrlsm  35861  lnmepi  35863  filnm  35868  gsumlsscl  39442  lincellss  39493  ellcoellss  39502
  Copyright terms: Public domain W3C validator