Theorem lssss 20842

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044   ⊆ wss 3914  ∅c0 4296  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  +_gcplusg 17220  Scalarcsca 17223   ·_𝑠 cvsca 17224  LSubSpclss 20837

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 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-ov 7390  df-lss 20838

This theorem is referenced by:  lssel  20843  lssuni  20845  00lss  20847  lsssubg  20863  islss3  20865  lsslss  20867  lssintcl  20870  lssmre  20872  lssacs  20873  lspid  20888  lspssv  20889  lspssp  20894  lsslsp  20921  lsslspOLD  20922  lmhmima  20954  reslmhm  20959  lsmsp  20993  pj1lmhm  21007  lsppratlem2  21058  lsppratlem3  21059  lsppratlem4  21060  lspprat  21063  lbsextlem3  21070  lidlss  21122  ocvin  21583  pjdm2  21620  pjff  21621  pjf2  21623  pjfo  21624  pjcss  21625  frlmgsum  21681  frlmsplit2  21682  lsslindf  21739  lsslinds  21740  cphsscph  25151  lssbn  25252  minveclem1  25324  minveclem2  25326  minveclem3a  25327  minveclem3b  25328  minveclem3  25329  minveclem4a  25330  minveclem4b  25331  minveclem4  25332  minveclem6  25334  minveclem7  25335  pjthlem1  25337  pjthlem2  25338  pjth  25339  lssdimle  33603  ply1degltdimlem  33618  ply1degltdim  33619  dimlssid  33628  islshpsm  38973  lshpnelb  38977  lshpnel2N  38978  lshpcmp  38981  lsatssv  38991  lssats  39005  lpssat  39006  lssatle  39008  lssat  39009  islshpcv  39046  lkrssv  39089  lkrlsp  39095  dvhopellsm  41111  dvadiaN  41122  dihss  41245  dihrnss  41272  dochord2N  41365  dochord3  41366  dihoml4  41371  dochsat  41377  dochshpncl  41378  dochnoncon  41385  djhlsmcl  41408  dihjat1lem  41422  dochsatshp  41445  dochsatshpb  41446  dochshpsat  41448  dochexmidlem2  41455  dochexmidlem5  41458  dochexmidlem6  41459  dochexmidlem7  41460  dochexmidlem8  41461  lclkrlem2p  41516  lclkrlem2v  41522  lcfrlem5  41540  lcfr  41579  mapdpglem17N  41682  mapdpglem18  41683  mapdpglem21  41686  islssfg  43059  islssfg2  43060  lnmlsslnm  43070  kercvrlsm  43072  lnmepi  43074  filnm  43079  gsumlsscl  48368  lincellss  48415  ellcoellss  48424