Theorem lssss 20990

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141   ≠ wne 2956  ∀wral 3075   ⊆ wss 3902  ∅c0 4283  ‘cfv 6515  (class class class)co 7390  Basecbs 17235  +_gcplusg 17276  Scalarcsca 17279   ·_𝑠 cvsca 17280  LSubSpclss 20985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-iota 6471  df-fun 6517  df-fv 6523  df-ov 7393  df-lss 20986

This theorem is referenced by:  lssel  20991  lssuni  20993  00lss  20995  lsssubg  21011  islss3  21013  lsslss  21015  lssintcl  21018  lssmre  21020  lssacs  21021  lspid  21036  lspssv  21037  lspssp  21042  lsslsp  21069  lmhmima  21101  reslmhm  21106  lsmsp  21140  pj1lmhm  21154  lsppratlem2  21205  lsppratlem3  21206  lsppratlem4  21207  lspprat  21210  lbsextlem3  21217  lidlss  21269  ocvin  21713  pjdm2  21750  pjff  21751  pjf2  21753  pjfo  21754  pjcss  21755  frlmgsum  21811  frlmsplit2  21812  lsslindf  21869  lsslinds  21870  cphsscph  25300  lssbn  25401  minveclem1  25473  minveclem2  25475  minveclem3a  25476  minveclem3b  25477  minveclem3  25478  minveclem4a  25479  minveclem4b  25480  minveclem4  25481  minveclem6  25483  minveclem7  25484  pjthlem1  25486  pjthlem2  25487  pjth  25488  lssdimle  33865  ply1degltdimlem  33879  ply1degltdim  33880  dimlssid  33889  islshpsm  39564  lshpnelb  39568  lshpnel2N  39569  lshpcmp  39572  lsatssv  39582  lssats  39596  lpssat  39597  lssatle  39599  lssat  39600  islshpcv  39637  lkrssv  39680  lkrlsp  39686  dvhopellsm  41701  dvadiaN  41712  dihss  41835  dihrnss  41862  dochord2N  41955  dochord3  41956  dihoml4  41961  dochsat  41967  dochshpncl  41968  dochnoncon  41975  djhlsmcl  41998  dihjat1lem  42012  dochsatshp  42035  dochsatshpb  42036  dochshpsat  42038  dochexmidlem2  42045  dochexmidlem5  42048  dochexmidlem6  42049  dochexmidlem7  42050  dochexmidlem8  42051  lclkrlem2p  42106  lclkrlem2v  42112  lcfrlem5  42130  lcfr  42169  mapdpglem17N  42272  mapdpglem18  42273  mapdpglem21  42276  islssfg  43607  islssfg2  43608  lnmlsslnm  43618  kercvrlsm  43620  lnmepi  43622  filnm  43627  gsumlsscl  48962  lincellss  49008  ellcoellss  49017