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

Theorem lssss 17901
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 2402 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
2 eqid 2402 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
3 lssss.v . . 3  |-  V  =  ( Base `  W
)
4 eqid 2402 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
5 eqid 2402 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
6 lssss.s . . 3  |-  S  =  ( LSubSp `  W )
71, 2, 3, 4, 5, 6islss 17899 . 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 1012 1  |-  ( U  e.  S  ->  U  C_  V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1405    e. wcel 1842    =/= wne 2598   A.wral 2753    C_ wss 3413   (/)c0 3737   ` cfv 5568  (class class class)co 6277   Basecbs 14839   +g cplusg 14907  Scalarcsca 14910   .scvsca 14911   LSubSpclss 17896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-iota 5532  df-fun 5570  df-fv 5576  df-ov 6280  df-lss 17897
This theorem is referenced by:  lssel  17902  lssuni  17904  00lss  17906  lsssubg  17921  islss3  17923  lsslss  17925  lssintcl  17928  lssmre  17930  lssacs  17931  lspid  17946  lspssv  17947  lspssp  17952  lsslsp  17979  lmhmima  18011  reslmhm  18016  lsmsp  18050  pj1lmhm  18064  lsppratlem2  18112  lsppratlem3  18113  lsppratlem4  18114  lspprat  18117  lbsextlem3  18124  lidlss  18174  ocvin  19001  pjdm2  19038  pjff  19039  pjf2  19041  pjfo  19042  pjcss  19043  frlmgsumOLD  19095  frlmgsum  19096  frlmsplit2  19097  lsslindf  19155  lsslinds  19156  lssbn  22080  minveclem1  22129  minveclem2  22131  minveclem3a  22132  minveclem3b  22133  minveclem3  22134  minveclem4a  22135  minveclem4b  22136  minveclem4  22137  minveclem6  22139  minveclem7  22140  pjthlem1  22142  pjthlem2  22143  pjth  22144  islshpsm  31978  lshpnelb  31982  lshpnel2N  31983  lshpcmp  31986  lsatssv  31996  lssats  32010  lpssat  32011  lssatle  32013  lssat  32014  islshpcv  32051  lkrssv  32094  lkrlsp  32100  dvhopellsm  34117  dvadiaN  34128  dihss  34251  dihrnss  34278  dochord2N  34371  dochord3  34372  dihoml4  34377  dochsat  34383  dochshpncl  34384  dochnoncon  34391  djhlsmcl  34414  dihjat1lem  34428  dochsatshp  34451  dochsatshpb  34452  dochshpsat  34454  dochexmidlem2  34461  dochexmidlem5  34464  dochexmidlem6  34465  dochexmidlem7  34466  dochexmidlem8  34467  lclkrlem2p  34522  lclkrlem2v  34528  lcfrlem5  34546  lcfr  34585  mapdpglem17N  34688  mapdpglem18  34689  mapdpglem21  34692  islssfg  35358  islssfg2  35359  lnmlsslnm  35369  kercvrlsm  35371  lnmepi  35373  filnm  35378  gsumlsscl  38468  lincellss  38519  ellcoellss  38528
  Copyright terms: Public domain W3C validator