Theorem lssss 20873

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ≠ wne 2929  ∀wral 3048   ⊆ wss 3898  ∅c0 4282  ‘cfv 6488  (class class class)co 7354  Basecbs 17124  +_gcplusg 17165  Scalarcsca 17168   ·_𝑠 cvsca 17169  LSubSpclss 20868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-iota 6444  df-fun 6490  df-fv 6496  df-ov 7357  df-lss 20869

This theorem is referenced by:  lssel  20874  lssuni  20876  00lss  20878  lsssubg  20894  islss3  20896  lsslss  20898  lssintcl  20901  lssmre  20903  lssacs  20904  lspid  20919  lspssv  20920  lspssp  20925  lsslsp  20952  lsslspOLD  20953  lmhmima  20985  reslmhm  20990  lsmsp  21024  pj1lmhm  21038  lsppratlem2  21089  lsppratlem3  21090  lsppratlem4  21091  lspprat  21094  lbsextlem3  21101  lidlss  21153  ocvin  21615  pjdm2  21652  pjff  21653  pjf2  21655  pjfo  21656  pjcss  21657  frlmgsum  21713  frlmsplit2  21714  lsslindf  21771  lsslinds  21772  cphsscph  25181  lssbn  25282  minveclem1  25354  minveclem2  25356  minveclem3a  25357  minveclem3b  25358  minveclem3  25359  minveclem4a  25360  minveclem4b  25361  minveclem4  25362  minveclem6  25364  minveclem7  25365  pjthlem1  25367  pjthlem2  25368  pjth  25369  lssdimle  33643  ply1degltdimlem  33658  ply1degltdim  33659  dimlssid  33668  islshpsm  39102  lshpnelb  39106  lshpnel2N  39107  lshpcmp  39110  lsatssv  39120  lssats  39134  lpssat  39135  lssatle  39137  lssat  39138  islshpcv  39175  lkrssv  39218  lkrlsp  39224  dvhopellsm  41239  dvadiaN  41250  dihss  41373  dihrnss  41400  dochord2N  41493  dochord3  41494  dihoml4  41499  dochsat  41505  dochshpncl  41506  dochnoncon  41513  djhlsmcl  41536  dihjat1lem  41550  dochsatshp  41573  dochsatshpb  41574  dochshpsat  41576  dochexmidlem2  41583  dochexmidlem5  41586  dochexmidlem6  41587  dochexmidlem7  41588  dochexmidlem8  41589  lclkrlem2p  41644  lclkrlem2v  41650  lcfrlem5  41668  lcfr  41707  mapdpglem17N  41810  mapdpglem18  41811  mapdpglem21  41814  islssfg  43190  islssfg2  43191  lnmlsslnm  43201  kercvrlsm  43203  lnmepi  43205  filnm  43210  gsumlsscl  48507  lincellss  48554  ellcoellss  48563