Theorem lssss 20952

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 2735	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
2		eqid 2735	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
3		lssss.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
4		eqid 2735	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
5		eqid 2735	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
6		lssss.s	. . 3 ⊢ 𝑆 = (LSubSp‘𝑊)
7	1, 2, 3, 4, 5, 6	islss 20950	. 2 ⊢ (𝑈 ∈ 𝑆 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥( ·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑈))
8	7	simp1bi 1144	1 ⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106   ≠ wne 2938  ∀wral 3059   ⊆ wss 3963  ∅c0 4339  ‘cfv 6563  (class class class)co 7431  Basecbs 17245  +_gcplusg 17298  Scalarcsca 17301   ·_𝑠 cvsca 17302  LSubSpclss 20947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-iota 6516  df-fun 6565  df-fv 6571  df-ov 7434  df-lss 20948

This theorem is referenced by:  lssel  20953  lssuni  20955  00lss  20957  lsssubg  20973  islss3  20975  lsslss  20977  lssintcl  20980  lssmre  20982  lssacs  20983  lspid  20998  lspssv  20999  lspssp  21004  lsslsp  21031  lsslspOLD  21032  lmhmima  21064  reslmhm  21069  lsmsp  21103  pj1lmhm  21117  lsppratlem2  21168  lsppratlem3  21169  lsppratlem4  21170  lspprat  21173  lbsextlem3  21180  lidlss  21240  ocvin  21710  pjdm2  21749  pjff  21750  pjf2  21752  pjfo  21753  pjcss  21754  frlmgsum  21810  frlmsplit2  21811  lsslindf  21868  lsslinds  21869  cphsscph  25299  lssbn  25400  minveclem1  25472  minveclem2  25474  minveclem3a  25475  minveclem3b  25476  minveclem3  25477  minveclem4a  25478  minveclem4b  25479  minveclem4  25480  minveclem6  25482  minveclem7  25483  pjthlem1  25485  pjthlem2  25486  pjth  25487  lssdimle  33635  ply1degltdimlem  33650  ply1degltdim  33651  dimlssid  33660  islshpsm  38962  lshpnelb  38966  lshpnel2N  38967  lshpcmp  38970  lsatssv  38980  lssats  38994  lpssat  38995  lssatle  38997  lssat  38998  islshpcv  39035  lkrssv  39078  lkrlsp  39084  dvhopellsm  41100  dvadiaN  41111  dihss  41234  dihrnss  41261  dochord2N  41354  dochord3  41355  dihoml4  41360  dochsat  41366  dochshpncl  41367  dochnoncon  41374  djhlsmcl  41397  dihjat1lem  41411  dochsatshp  41434  dochsatshpb  41435  dochshpsat  41437  dochexmidlem2  41444  dochexmidlem5  41447  dochexmidlem6  41448  dochexmidlem7  41449  dochexmidlem8  41450  lclkrlem2p  41505  lclkrlem2v  41511  lcfrlem5  41529  lcfr  41568  mapdpglem17N  41671  mapdpglem18  41672  mapdpglem21  41675  islssfg  43059  islssfg2  43060  lnmlsslnm  43070  kercvrlsm  43072  lnmepi  43074  filnm  43079  gsumlsscl  48225  lincellss  48272  ellcoellss  48281