Theorem lssss 19776

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∀wral 3070   ⊆ wss 3858  ∅c0 4225  ‘cfv 6335  (class class class)co 7150  Basecbs 16541  +_gcplusg 16623  Scalarcsca 16626   ·_𝑠 cvsca 16627  LSubSpclss 19771

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-iota 6294  df-fun 6337  df-fv 6343  df-ov 7153  df-lss 19772

This theorem is referenced by:  lssel  19777  lssuni  19779  00lss  19781  lsssubg  19797  islss3  19799  lsslss  19801  lssintcl  19804  lssmre  19806  lssacs  19807  lspid  19822  lspssv  19823  lspssp  19828  lsslsp  19855  lmhmima  19887  reslmhm  19892  lsmsp  19926  pj1lmhm  19940  lsppratlem2  19988  lsppratlem3  19989  lsppratlem4  19990  lspprat  19993  lbsextlem3  20000  lidlss  20051  ocvin  20439  pjdm2  20476  pjff  20477  pjf2  20479  pjfo  20480  pjcss  20481  frlmgsum  20537  frlmsplit2  20538  lsslindf  20595  lsslinds  20596  cphsscph  23951  lssbn  24052  minveclem1  24124  minveclem2  24126  minveclem3a  24127  minveclem3b  24128  minveclem3  24129  minveclem4a  24130  minveclem4b  24131  minveclem4  24132  minveclem6  24134  minveclem7  24135  pjthlem1  24137  pjthlem2  24138  pjth  24139  lssdimle  31212  islshpsm  36556  lshpnelb  36560  lshpnel2N  36561  lshpcmp  36564  lsatssv  36574  lssats  36588  lpssat  36589  lssatle  36591  lssat  36592  islshpcv  36629  lkrssv  36672  lkrlsp  36678  dvhopellsm  38693  dvadiaN  38704  dihss  38827  dihrnss  38854  dochord2N  38947  dochord3  38948  dihoml4  38953  dochsat  38959  dochshpncl  38960  dochnoncon  38967  djhlsmcl  38990  dihjat1lem  39004  dochsatshp  39027  dochsatshpb  39028  dochshpsat  39030  dochexmidlem2  39037  dochexmidlem5  39040  dochexmidlem6  39041  dochexmidlem7  39042  dochexmidlem8  39043  lclkrlem2p  39098  lclkrlem2v  39104  lcfrlem5  39122  lcfr  39161  mapdpglem17N  39264  mapdpglem18  39265  mapdpglem21  39268  islssfg  40387  islssfg2  40388  lnmlsslnm  40398  kercvrlsm  40400  lnmepi  40402  filnm  40407  gsumlsscl  45152  lincellss  45200  ellcoellss  45209