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

Theorem lssss 16018
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 2438 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
2 eqid 2438 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
3 lssss.v . . 3  |-  V  =  ( Base `  W
)
4 eqid 2438 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
5 eqid 2438 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
6 lssss.s . . 3  |-  S  =  ( LSubSp `  W )
71, 2, 3, 4, 5, 6islss 16016 . 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 973 1  |-  ( U  e.  S  ->  U  C_  V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726    =/= wne 2601   A.wral 2707    C_ wss 3322   (/)c0 3630   ` cfv 5457  (class class class)co 6084   Basecbs 13474   +g cplusg 13534  Scalarcsca 13537   .scvsca 13538   LSubSpclss 16013
This theorem is referenced by:  lssel  16019  lssuni  16021  00lss  16023  lsssubg  16038  islss3  16040  lsslss  16042  lssintcl  16045  lssmre  16047  lssacs  16048  lspid  16063  lspssv  16064  lspssp  16069  lsslsp  16096  lmhmima  16128  reslmhm  16133  lsmsp  16163  pj1lmhm  16177  lsppratlem2  16225  lsppratlem3  16226  lsppratlem4  16227  lspprat  16230  lbsextlem3  16237  lidlss  16285  ocvin  16906  pjdm2  16943  pjff  16944  pjf2  16946  pjfo  16947  pjcss  16948  lssbn  19309  minveclem1  19330  minveclem2  19332  minveclem3a  19333  minveclem3b  19334  minveclem3  19335  minveclem4a  19336  minveclem4b  19337  minveclem4  19338  minveclem6  19340  minveclem7  19341  pjthlem1  19343  pjthlem2  19344  pjth  19345  islssfg  27158  islssfg2  27159  lnmlsslnm  27169  kercvrlsm  27171  lnmepi  27173  filnm  27182  frlmgsum  27222  frlmsplit2  27233  lsslindf  27290  lsslinds  27291  islshpsm  29851  lshpnelb  29855  lshpnel2N  29856  lshpcmp  29859  lsatssv  29869  lssats  29883  lpssat  29884  lssatle  29886  lssat  29887  islshpcv  29924  lkrssv  29967  lkrlsp  29973  dvhopellsm  31988  dvadiaN  31999  dihss  32122  dihrnss  32149  dochord2N  32242  dochord3  32243  dihoml4  32248  dochsat  32254  dochshpncl  32255  dochnoncon  32262  djhlsmcl  32285  dihjat1lem  32299  dochsatshp  32322  dochsatshpb  32323  dochshpsat  32325  dochexmidlem2  32332  dochexmidlem5  32335  dochexmidlem6  32336  dochexmidlem7  32337  dochexmidlem8  32338  lclkrlem2p  32393  lclkrlem2v  32399  lcfrlem5  32417  lcfr  32456  mapdpglem17N  32559  mapdpglem18  32560  mapdpglem21  32563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-iota 5421  df-fun 5459  df-fv 5465  df-ov 6087  df-lss 16014
  Copyright terms: Public domain W3C validator