Theorem lssss 20907

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   ≠ wne 2931  ∀wral 3050   ⊆ wss 3933  ∅c0 4315  ‘cfv 6542  (class class class)co 7414  Basecbs 17230  +_gcplusg 17277  Scalarcsca 17280   ·_𝑠 cvsca 17281  LSubSpclss 20902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pow 5347  ax-pr 5414

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-opab 5188  df-mpt 5208  df-id 5560  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-iota 6495  df-fun 6544  df-fv 6550  df-ov 7417  df-lss 20903

This theorem is referenced by:  lssel  20908  lssuni  20910  00lss  20912  lsssubg  20928  islss3  20930  lsslss  20932  lssintcl  20935  lssmre  20937  lssacs  20938  lspid  20953  lspssv  20954  lspssp  20959  lsslsp  20986  lsslspOLD  20987  lmhmima  21019  reslmhm  21024  lsmsp  21058  pj1lmhm  21072  lsppratlem2  21123  lsppratlem3  21124  lsppratlem4  21125  lspprat  21128  lbsextlem3  21135  lidlss  21189  ocvin  21659  pjdm2  21698  pjff  21699  pjf2  21701  pjfo  21702  pjcss  21703  frlmgsum  21759  frlmsplit2  21760  lsslindf  21817  lsslinds  21818  cphsscph  25240  lssbn  25341  minveclem1  25413  minveclem2  25415  minveclem3a  25416  minveclem3b  25417  minveclem3  25418  minveclem4a  25419  minveclem4b  25420  minveclem4  25421  minveclem6  25423  minveclem7  25424  pjthlem1  25426  pjthlem2  25427  pjth  25428  lssdimle  33599  ply1degltdimlem  33614  ply1degltdim  33615  dimlssid  33624  islshpsm  38922  lshpnelb  38926  lshpnel2N  38927  lshpcmp  38930  lsatssv  38940  lssats  38954  lpssat  38955  lssatle  38957  lssat  38958  islshpcv  38995  lkrssv  39038  lkrlsp  39044  dvhopellsm  41060  dvadiaN  41071  dihss  41194  dihrnss  41221  dochord2N  41314  dochord3  41315  dihoml4  41320  dochsat  41326  dochshpncl  41327  dochnoncon  41334  djhlsmcl  41357  dihjat1lem  41371  dochsatshp  41394  dochsatshpb  41395  dochshpsat  41397  dochexmidlem2  41404  dochexmidlem5  41407  dochexmidlem6  41408  dochexmidlem7  41409  dochexmidlem8  41410  lclkrlem2p  41465  lclkrlem2v  41471  lcfrlem5  41489  lcfr  41528  mapdpglem17N  41631  mapdpglem18  41632  mapdpglem21  41635  islssfg  43027  islssfg2  43028  lnmlsslnm  43038  kercvrlsm  43040  lnmepi  43042  filnm  43047  gsumlsscl  48242  lincellss  48289  ellcoellss  48298