Theorem lssss 20898

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ≠ wne 2933  ∀wral 3052   ⊆ wss 3931  ∅c0 4313  ‘cfv 6536  (class class class)co 7410  Basecbs 17233  +_gcplusg 17276  Scalarcsca 17279   ·_𝑠 cvsca 17280  LSubSpclss 20893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6489  df-fun 6538  df-fv 6544  df-ov 7413  df-lss 20894

This theorem is referenced by:  lssel  20899  lssuni  20901  00lss  20903  lsssubg  20919  islss3  20921  lsslss  20923  lssintcl  20926  lssmre  20928  lssacs  20929  lspid  20944  lspssv  20945  lspssp  20950  lsslsp  20977  lsslspOLD  20978  lmhmima  21010  reslmhm  21015  lsmsp  21049  pj1lmhm  21063  lsppratlem2  21114  lsppratlem3  21115  lsppratlem4  21116  lspprat  21119  lbsextlem3  21126  lidlss  21178  ocvin  21639  pjdm2  21676  pjff  21677  pjf2  21679  pjfo  21680  pjcss  21681  frlmgsum  21737  frlmsplit2  21738  lsslindf  21795  lsslinds  21796  cphsscph  25208  lssbn  25309  minveclem1  25381  minveclem2  25383  minveclem3a  25384  minveclem3b  25385  minveclem3  25386  minveclem4a  25387  minveclem4b  25388  minveclem4  25389  minveclem6  25391  minveclem7  25392  pjthlem1  25394  pjthlem2  25395  pjth  25396  lssdimle  33652  ply1degltdimlem  33667  ply1degltdim  33668  dimlssid  33677  islshpsm  39003  lshpnelb  39007  lshpnel2N  39008  lshpcmp  39011  lsatssv  39021  lssats  39035  lpssat  39036  lssatle  39038  lssat  39039  islshpcv  39076  lkrssv  39119  lkrlsp  39125  dvhopellsm  41141  dvadiaN  41152  dihss  41275  dihrnss  41302  dochord2N  41395  dochord3  41396  dihoml4  41401  dochsat  41407  dochshpncl  41408  dochnoncon  41415  djhlsmcl  41438  dihjat1lem  41452  dochsatshp  41475  dochsatshpb  41476  dochshpsat  41478  dochexmidlem2  41485  dochexmidlem5  41488  dochexmidlem6  41489  dochexmidlem7  41490  dochexmidlem8  41491  lclkrlem2p  41546  lclkrlem2v  41552  lcfrlem5  41570  lcfr  41609  mapdpglem17N  41712  mapdpglem18  41713  mapdpglem21  41716  islssfg  43069  islssfg2  43070  lnmlsslnm  43080  kercvrlsm  43082  lnmepi  43084  filnm  43089  gsumlsscl  48335  lincellss  48382  ellcoellss  48391