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

Theorem lssss 17126
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 2451 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
2 eqid 2451 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
3 lssss.v . . 3  |-  V  =  ( Base `  W
)
4 eqid 2451 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
5 eqid 2451 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
6 lssss.s . . 3  |-  S  =  ( LSubSp `  W )
71, 2, 3, 4, 5, 6islss 17124 . 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 1003 1  |-  ( U  e.  S  ->  U  C_  V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758    =/= wne 2644   A.wral 2795    C_ wss 3428   (/)c0 3737   ` cfv 5518  (class class class)co 6192   Basecbs 14278   +g cplusg 14342  Scalarcsca 14345   .scvsca 14346   LSubSpclss 17121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4513  ax-nul 4521  ax-pow 4570  ax-pr 4631
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3072  df-sbc 3287  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-pw 3962  df-sn 3978  df-pr 3980  df-op 3984  df-uni 4192  df-br 4393  df-opab 4451  df-mpt 4452  df-id 4736  df-xp 4946  df-rel 4947  df-cnv 4948  df-co 4949  df-dm 4950  df-iota 5481  df-fun 5520  df-fv 5526  df-ov 6195  df-lss 17122
This theorem is referenced by:  lssel  17127  lssuni  17129  00lss  17131  lsssubg  17146  islss3  17148  lsslss  17150  lssintcl  17153  lssmre  17155  lssacs  17156  lspid  17171  lspssv  17172  lspssp  17177  lsslsp  17204  lmhmima  17236  reslmhm  17241  lsmsp  17275  pj1lmhm  17289  lsppratlem2  17337  lsppratlem3  17338  lsppratlem4  17339  lspprat  17342  lbsextlem3  17349  lidlss  17399  ocvin  18210  pjdm2  18247  pjff  18248  pjf2  18250  pjfo  18251  pjcss  18252  frlmgsumOLD  18306  frlmgsum  18307  frlmsplit2  18308  lsslindf  18370  lsslinds  18371  lssbn  20980  minveclem1  21029  minveclem2  21031  minveclem3a  21032  minveclem3b  21033  minveclem3  21034  minveclem4a  21035  minveclem4b  21036  minveclem4  21037  minveclem6  21039  minveclem7  21040  pjthlem1  21042  pjthlem2  21043  pjth  21044  islssfg  29563  islssfg2  29564  lnmlsslnm  29574  kercvrlsm  29576  lnmepi  29578  filnm  29583  gsumlsscl  30960  lincellss  31069  ellcoellss  31078  islshpsm  32933  lshpnelb  32937  lshpnel2N  32938  lshpcmp  32941  lsatssv  32951  lssats  32965  lpssat  32966  lssatle  32968  lssat  32969  islshpcv  33006  lkrssv  33049  lkrlsp  33055  dvhopellsm  35070  dvadiaN  35081  dihss  35204  dihrnss  35231  dochord2N  35324  dochord3  35325  dihoml4  35330  dochsat  35336  dochshpncl  35337  dochnoncon  35344  djhlsmcl  35367  dihjat1lem  35381  dochsatshp  35404  dochsatshpb  35405  dochshpsat  35407  dochexmidlem2  35414  dochexmidlem5  35417  dochexmidlem6  35418  dochexmidlem7  35419  dochexmidlem8  35420  lclkrlem2p  35475  lclkrlem2v  35481  lcfrlem5  35499  lcfr  35538  mapdpglem17N  35641  mapdpglem18  35642  mapdpglem21  35645
  Copyright terms: Public domain W3C validator