Theorem lssss 20922

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052   ⊆ wss 3890  ∅c0 4274  ‘cfv 6492  (class class class)co 7360  Basecbs 17170  +_gcplusg 17211  Scalarcsca 17214   ·_𝑠 cvsca 17215  LSubSpclss 20917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7363  df-lss 20918

This theorem is referenced by:  lssel  20923  lssuni  20925  00lss  20927  lsssubg  20943  islss3  20945  lsslss  20947  lssintcl  20950  lssmre  20952  lssacs  20953  lspid  20968  lspssv  20969  lspssp  20974  lsslsp  21001  lsslspOLD  21002  lmhmima  21034  reslmhm  21039  lsmsp  21073  pj1lmhm  21087  lsppratlem2  21138  lsppratlem3  21139  lsppratlem4  21140  lspprat  21143  lbsextlem3  21150  lidlss  21202  ocvin  21664  pjdm2  21701  pjff  21702  pjf2  21704  pjfo  21705  pjcss  21706  frlmgsum  21762  frlmsplit2  21763  lsslindf  21820  lsslinds  21821  cphsscph  25228  lssbn  25329  minveclem1  25401  minveclem2  25403  minveclem3a  25404  minveclem3b  25405  minveclem3  25406  minveclem4a  25407  minveclem4b  25408  minveclem4  25409  minveclem6  25411  minveclem7  25412  pjthlem1  25414  pjthlem2  25415  pjth  25416  lssdimle  33767  ply1degltdimlem  33782  ply1degltdim  33783  dimlssid  33792  islshpsm  39440  lshpnelb  39444  lshpnel2N  39445  lshpcmp  39448  lsatssv  39458  lssats  39472  lpssat  39473  lssatle  39475  lssat  39476  islshpcv  39513  lkrssv  39556  lkrlsp  39562  dvhopellsm  41577  dvadiaN  41588  dihss  41711  dihrnss  41738  dochord2N  41831  dochord3  41832  dihoml4  41837  dochsat  41843  dochshpncl  41844  dochnoncon  41851  djhlsmcl  41874  dihjat1lem  41888  dochsatshp  41911  dochsatshpb  41912  dochshpsat  41914  dochexmidlem2  41921  dochexmidlem5  41924  dochexmidlem6  41925  dochexmidlem7  41926  dochexmidlem8  41927  lclkrlem2p  41982  lclkrlem2v  41988  lcfrlem5  42006  lcfr  42045  mapdpglem17N  42148  mapdpglem18  42149  mapdpglem21  42152  islssfg  43516  islssfg2  43517  lnmlsslnm  43527  kercvrlsm  43529  lnmepi  43531  filnm  43536  gsumlsscl  48868  lincellss  48914  ellcoellss  48923