Theorem lssss 20933

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.

Step	Hyp	Ref	Expression
1		eqid 2740	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
2		eqid 2740	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
3		lssss.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
4		eqid 2740	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
5		eqid 2740	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
6		lssss.s	. . 3 ⊢ 𝑆 = (LSubSp‘𝑊)
7	1, 2, 3, 4, 5, 6	islss 20931	. 2 ⊢ (𝑈 ∈ 𝑆 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥( ·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑈))
8	7	simp1bi 1151	1 ⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ≠ wne 2935  ∀wral 3054   ⊆ wss 3890  ∅c0 4268  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  +_gcplusg 17218  Scalarcsca 17221   ·_𝑠 cvsca 17222  LSubSpclss 20928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7366  df-lss 20929

This theorem is referenced by:  lssel  20934  lssuni  20936  00lss  20938  lsssubg  20954  islss3  20956  lsslss  20958  lssintcl  20961  lssmre  20963  lssacs  20964  lspid  20979  lspssv  20980  lspssp  20985  lsslsp  21012  lmhmima  21044  reslmhm  21049  lsmsp  21083  pj1lmhm  21097  lsppratlem2  21148  lsppratlem3  21149  lsppratlem4  21150  lspprat  21153  lbsextlem3  21160  lidlss  21212  ocvin  21656  pjdm2  21693  pjff  21694  pjf2  21696  pjfo  21697  pjcss  21698  frlmgsum  21754  frlmsplit2  21755  lsslindf  21812  lsslinds  21813  cphsscph  25243  lssbn  25344  minveclem1  25416  minveclem2  25418  minveclem3a  25419  minveclem3b  25420  minveclem3  25421  minveclem4a  25422  minveclem4b  25423  minveclem4  25424  minveclem6  25426  minveclem7  25427  pjthlem1  25429  pjthlem2  25430  pjth  25431  lssdimle  33799  ply1degltdimlem  33813  ply1degltdim  33814  dimlssid  33823  islshpsm  39479  lshpnelb  39483  lshpnel2N  39484  lshpcmp  39487  lsatssv  39497  lssats  39511  lpssat  39512  lssatle  39514  lssat  39515  islshpcv  39552  lkrssv  39595  lkrlsp  39601  dvhopellsm  41616  dvadiaN  41627  dihss  41750  dihrnss  41777  dochord2N  41870  dochord3  41871  dihoml4  41876  dochsat  41882  dochshpncl  41883  dochnoncon  41890  djhlsmcl  41913  dihjat1lem  41927  dochsatshp  41950  dochsatshpb  41951  dochshpsat  41953  dochexmidlem2  41960  dochexmidlem5  41963  dochexmidlem6  41964  dochexmidlem7  41965  dochexmidlem8  41966  lclkrlem2p  42021  lclkrlem2v  42027  lcfrlem5  42045  lcfr  42084  mapdpglem17N  42187  mapdpglem18  42188  mapdpglem21  42191  islssfg  43522  islssfg2  43523  lnmlsslnm  43533  kercvrlsm  43535  lnmepi  43537  filnm  43542  gsumlsscl  48878  lincellss  48924  ellcoellss  48933