Theorem lssss 20539

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ≠ wne 2940  ∀wral 3061   ⊆ wss 3947  ∅c0 4321  ‘cfv 6540  (class class class)co 7405  Basecbs 17140  +_gcplusg 17193  Scalarcsca 17196   ·_𝑠 cvsca 17197  LSubSpclss 20534

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6492  df-fun 6542  df-fv 6548  df-ov 7408  df-lss 20535

This theorem is referenced by:  lssel  20540  lssuni  20542  00lss  20544  lsssubg  20560  islss3  20562  lsslss  20564  lssintcl  20567  lssmre  20569  lssacs  20570  lspid  20585  lspssv  20586  lspssp  20591  lsslsp  20618  lmhmima  20650  reslmhm  20655  lsmsp  20689  pj1lmhm  20703  lsppratlem2  20753  lsppratlem3  20754  lsppratlem4  20755  lspprat  20758  lbsextlem3  20765  lidlss  20825  ocvin  21218  pjdm2  21257  pjff  21258  pjf2  21260  pjfo  21261  pjcss  21262  frlmgsum  21318  frlmsplit2  21319  lsslindf  21376  lsslinds  21377  cphsscph  24759  lssbn  24860  minveclem1  24932  minveclem2  24934  minveclem3a  24935  minveclem3b  24936  minveclem3  24937  minveclem4a  24938  minveclem4b  24939  minveclem4  24940  minveclem6  24942  minveclem7  24943  pjthlem1  24945  pjthlem2  24946  pjth  24947  lssdimle  32680  ply1degltdimlem  32695  ply1degltdim  32696  islshpsm  37838  lshpnelb  37842  lshpnel2N  37843  lshpcmp  37846  lsatssv  37856  lssats  37870  lpssat  37871  lssatle  37873  lssat  37874  islshpcv  37911  lkrssv  37954  lkrlsp  37960  dvhopellsm  39976  dvadiaN  39987  dihss  40110  dihrnss  40137  dochord2N  40230  dochord3  40231  dihoml4  40236  dochsat  40242  dochshpncl  40243  dochnoncon  40250  djhlsmcl  40273  dihjat1lem  40287  dochsatshp  40310  dochsatshpb  40311  dochshpsat  40313  dochexmidlem2  40320  dochexmidlem5  40323  dochexmidlem6  40324  dochexmidlem7  40325  dochexmidlem8  40326  lclkrlem2p  40381  lclkrlem2v  40387  lcfrlem5  40405  lcfr  40444  mapdpglem17N  40547  mapdpglem18  40548  mapdpglem21  40551  islssfg  41797  islssfg2  41798  lnmlsslnm  41808  kercvrlsm  41810  lnmepi  41812  filnm  41817  gsumlsscl  47012  lincellss  47060  ellcoellss  47069