Theorem lssss 21031

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085   ⊆ wss 3913  ∅c0 4294  ‘cfv 6533  (class class class)co 7408  Basecbs 17265  +_gcplusg 17306  Scalarcsca 17309   ·_𝑠 cvsca 17310  LSubSpclss 21026

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6489  df-fun 6535  df-fv 6541  df-ov 7411  df-lss 21027

This theorem is referenced by:  lssel  21032  lssuni  21034  00lss  21036  lsssubg  21052  islss3  21054  lsslss  21056  lssintcl  21059  lssmre  21061  lssacs  21062  lspid  21077  lspssv  21078  lspssp  21083  lsslsp  21110  lmhmima  21142  reslmhm  21147  lsmsp  21181  pj1lmhm  21195  lsppratlem2  21246  lsppratlem3  21247  lsppratlem4  21248  lspprat  21251  lbsextlem3  21258  lidlss  21310  ocvin  21789  pjdm2  21826  pjff  21827  pjf2  21829  pjfo  21830  pjcss  21831  frlmgsum  21887  frlmsplit2  21888  lsslindf  21945  lsslinds  21946  cphsscph  25375  lssbn  25476  minveclem1  25548  minveclem2  25550  minveclem3a  25551  minveclem3b  25552  minveclem3  25553  minveclem4a  25554  minveclem4b  25555  minveclem4  25556  minveclem6  25558  minveclem7  25559  pjthlem1  25561  pjthlem2  25562  pjth  25563  lssdimle  33939  ply1degltdimlem  33953  ply1degltdim  33954  dimlssid  33963  islshpsm  39639  lshpnelb  39643  lshpnel2N  39644  lshpcmp  39647  lsatssv  39657  lssats  39671  lpssat  39672  lssatle  39674  lssat  39675  islshpcv  39712  lkrssv  39755  lkrlsp  39761  dvhopellsm  41776  dvadiaN  41787  dihss  41910  dihrnss  41937  dochord2N  42030  dochord3  42031  dihoml4  42036  dochsat  42042  dochshpncl  42043  dochnoncon  42050  djhlsmcl  42073  dihjat1lem  42087  dochsatshp  42110  dochsatshpb  42111  dochshpsat  42113  dochexmidlem2  42120  dochexmidlem5  42123  dochexmidlem6  42124  dochexmidlem7  42125  dochexmidlem8  42126  lclkrlem2p  42181  lclkrlem2v  42187  lcfrlem5  42205  lcfr  42244  mapdpglem17N  42347  mapdpglem18  42348  mapdpglem21  42351  islssfg  43682  islssfg2  43683  lnmlsslnm  43693  kercvrlsm  43695  lnmepi  43697  filnm  43702  gsumlsscl  49038  lincellss  49084  ellcoellss  49093