Theorem lssss 20547

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062   ⊆ wss 3949  ∅c0 4323  ‘cfv 6544  (class class class)co 7409  Basecbs 17144  +_gcplusg 17197  Scalarcsca 17200   ·_𝑠 cvsca 17201  LSubSpclss 20542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-iota 6496  df-fun 6546  df-fv 6552  df-ov 7412  df-lss 20543

This theorem is referenced by:  lssel  20548  lssuni  20550  00lss  20552  lsssubg  20568  islss3  20570  lsslss  20572  lssintcl  20575  lssmre  20577  lssacs  20578  lspid  20593  lspssv  20594  lspssp  20599  lsslsp  20626  lmhmima  20658  reslmhm  20663  lsmsp  20697  pj1lmhm  20711  lsppratlem2  20761  lsppratlem3  20762  lsppratlem4  20763  lspprat  20766  lbsextlem3  20773  lidlss  20833  ocvin  21227  pjdm2  21266  pjff  21267  pjf2  21269  pjfo  21270  pjcss  21271  frlmgsum  21327  frlmsplit2  21328  lsslindf  21385  lsslinds  21386  cphsscph  24768  lssbn  24869  minveclem1  24941  minveclem2  24943  minveclem3a  24944  minveclem3b  24945  minveclem3  24946  minveclem4a  24947  minveclem4b  24948  minveclem4  24949  minveclem6  24951  minveclem7  24952  pjthlem1  24954  pjthlem2  24955  pjth  24956  lssdimle  32692  ply1degltdimlem  32707  ply1degltdim  32708  islshpsm  37850  lshpnelb  37854  lshpnel2N  37855  lshpcmp  37858  lsatssv  37868  lssats  37882  lpssat  37883  lssatle  37885  lssat  37886  islshpcv  37923  lkrssv  37966  lkrlsp  37972  dvhopellsm  39988  dvadiaN  39999  dihss  40122  dihrnss  40149  dochord2N  40242  dochord3  40243  dihoml4  40248  dochsat  40254  dochshpncl  40255  dochnoncon  40262  djhlsmcl  40285  dihjat1lem  40299  dochsatshp  40322  dochsatshpb  40323  dochshpsat  40325  dochexmidlem2  40332  dochexmidlem5  40335  dochexmidlem6  40336  dochexmidlem7  40337  dochexmidlem8  40338  lclkrlem2p  40393  lclkrlem2v  40399  lcfrlem5  40417  lcfr  40456  mapdpglem17N  40559  mapdpglem18  40560  mapdpglem21  40563  islssfg  41812  islssfg2  41813  lnmlsslnm  41823  kercvrlsm  41825  lnmepi  41827  filnm  41832  gsumlsscl  47059  lincellss  47107  ellcoellss  47116