Theorem lssss 20870

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111   ≠ wne 2928  ∀wral 3047   ⊆ wss 3902  ∅c0 4283  ‘cfv 6481  (class class class)co 7346  Basecbs 17120  +_gcplusg 17161  Scalarcsca 17164   ·_𝑠 cvsca 17165  LSubSpclss 20865

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-iota 6437  df-fun 6483  df-fv 6489  df-ov 7349  df-lss 20866

This theorem is referenced by:  lssel  20871  lssuni  20873  00lss  20875  lsssubg  20891  islss3  20893  lsslss  20895  lssintcl  20898  lssmre  20900  lssacs  20901  lspid  20916  lspssv  20917  lspssp  20922  lsslsp  20949  lsslspOLD  20950  lmhmima  20982  reslmhm  20987  lsmsp  21021  pj1lmhm  21035  lsppratlem2  21086  lsppratlem3  21087  lsppratlem4  21088  lspprat  21091  lbsextlem3  21098  lidlss  21150  ocvin  21612  pjdm2  21649  pjff  21650  pjf2  21652  pjfo  21653  pjcss  21654  frlmgsum  21710  frlmsplit2  21711  lsslindf  21768  lsslinds  21769  cphsscph  25179  lssbn  25280  minveclem1  25352  minveclem2  25354  minveclem3a  25355  minveclem3b  25356  minveclem3  25357  minveclem4a  25358  minveclem4b  25359  minveclem4  25360  minveclem6  25362  minveclem7  25363  pjthlem1  25365  pjthlem2  25366  pjth  25367  lssdimle  33618  ply1degltdimlem  33633  ply1degltdim  33634  dimlssid  33643  islshpsm  39025  lshpnelb  39029  lshpnel2N  39030  lshpcmp  39033  lsatssv  39043  lssats  39057  lpssat  39058  lssatle  39060  lssat  39061  islshpcv  39098  lkrssv  39141  lkrlsp  39147  dvhopellsm  41162  dvadiaN  41173  dihss  41296  dihrnss  41323  dochord2N  41416  dochord3  41417  dihoml4  41422  dochsat  41428  dochshpncl  41429  dochnoncon  41436  djhlsmcl  41459  dihjat1lem  41473  dochsatshp  41496  dochsatshpb  41497  dochshpsat  41499  dochexmidlem2  41506  dochexmidlem5  41509  dochexmidlem6  41510  dochexmidlem7  41511  dochexmidlem8  41512  lclkrlem2p  41567  lclkrlem2v  41573  lcfrlem5  41591  lcfr  41630  mapdpglem17N  41733  mapdpglem18  41734  mapdpglem21  41737  islssfg  43109  islssfg2  43110  lnmlsslnm  43120  kercvrlsm  43122  lnmepi  43124  filnm  43129  gsumlsscl  48417  lincellss  48464  ellcoellss  48473