Theorem lssss 20899

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 20897	. 2 ⊢ (𝑈 ∈ 𝑆 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥( ·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑈))
8	7	simp1bi 1146	1 ⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052   ⊆ wss 3903  ∅c0 4287  ‘cfv 6500  (class class class)co 7368  Basecbs 17148  +_gcplusg 17189  Scalarcsca 17192   ·_𝑠 cvsca 17193  LSubSpclss 20894

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 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-ov 7371  df-lss 20895

This theorem is referenced by:  lssel  20900  lssuni  20902  00lss  20904  lsssubg  20920  islss3  20922  lsslss  20924  lssintcl  20927  lssmre  20929  lssacs  20930  lspid  20945  lspssv  20946  lspssp  20951  lsslsp  20978  lsslspOLD  20979  lmhmima  21011  reslmhm  21016  lsmsp  21050  pj1lmhm  21064  lsppratlem2  21115  lsppratlem3  21116  lsppratlem4  21117  lspprat  21120  lbsextlem3  21127  lidlss  21179  ocvin  21641  pjdm2  21678  pjff  21679  pjf2  21681  pjfo  21682  pjcss  21683  frlmgsum  21739  frlmsplit2  21740  lsslindf  21797  lsslinds  21798  cphsscph  25219  lssbn  25320  minveclem1  25392  minveclem2  25394  minveclem3a  25395  minveclem3b  25396  minveclem3  25397  minveclem4a  25398  minveclem4b  25399  minveclem4  25400  minveclem6  25402  minveclem7  25403  pjthlem1  25405  pjthlem2  25406  pjth  25407  lssdimle  33784  ply1degltdimlem  33799  ply1degltdim  33800  dimlssid  33809  islshpsm  39353  lshpnelb  39357  lshpnel2N  39358  lshpcmp  39361  lsatssv  39371  lssats  39385  lpssat  39386  lssatle  39388  lssat  39389  islshpcv  39426  lkrssv  39469  lkrlsp  39475  dvhopellsm  41490  dvadiaN  41501  dihss  41624  dihrnss  41651  dochord2N  41744  dochord3  41745  dihoml4  41750  dochsat  41756  dochshpncl  41757  dochnoncon  41764  djhlsmcl  41787  dihjat1lem  41801  dochsatshp  41824  dochsatshpb  41825  dochshpsat  41827  dochexmidlem2  41834  dochexmidlem5  41837  dochexmidlem6  41838  dochexmidlem7  41839  dochexmidlem8  41840  lclkrlem2p  41895  lclkrlem2v  41901  lcfrlem5  41919  lcfr  41958  mapdpglem17N  42061  mapdpglem18  42062  mapdpglem21  42065  islssfg  43424  islssfg2  43425  lnmlsslnm  43435  kercvrlsm  43437  lnmepi  43439  filnm  43444  gsumlsscl  48737  lincellss  48783  ellcoellss  48792