Theorem lssss 21120

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  ∀wral 3076   ⊆ wss 3899  ∅c0 4279  ‘cfv 6533  (class class class)co 7413  Basecbs 17301  +_gcplusg 17342  Scalarcsca 17345   ·_𝑠 cvsca 17346  LSubSpclss 21115

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6489  df-fun 6535  df-fv 6541  df-ov 7416  df-lss 21116

This theorem is used by:  lssel  21121  lssuni  21123  00lss  21125  lsssubg  21141  islss3  21143  lsslss  21145  lssintcl  21148  lssmre  21150  lssacs  21151  lspid  21166  lspssv  21167  lspssp  21172  lsslsp  21199  lmhmima  21231  reslmhm  21236  lsmsp  21270  pj1lmhm  21284  lsppratlem2  21335  lsppratlem3  21336  lsppratlem4  21337  lspprat  21340  lbsextlem3  21347  lidlss  21399  ocvin  21887  pjdm2  21924  pjff  21925  pjf2  21927  pjfo  21928  pjcss  21929  frlmgsum  21985  frlmsplit2  21986  lsslindf  22043  lsslinds  22044  cphsscph  25479  lssbn  25580  minveclem1  25652  minveclem2  25654  minveclem3a  25655  minveclem3b  25656  minveclem3  25657  minveclem4a  25658  minveclem4b  25659  minveclem4  25660  minveclem6  25662  minveclem7  25663  pjthlem1  25665  pjthlem2  25666  pjth  25667  lssdimle  34118  ply1degltdimlem  34132  ply1degltdim  34133  dimlssid  34142  islshpsm  39853  lshpnelb  39857  lshpnel2N  39858  lshpcmp  39861  lsatssv  39871  lssats  39885  lpssat  39886  lssatle  39888  lssat  39889  islshpcv  39926  lkrssv  39969  lkrlsp  39975  dvhopellsm  41990  dvadiaN  42001  dihss  42124  dihrnss  42151  dochord2N  42244  dochord3  42245  dihoml4  42250  dochsat  42256  dochshpncl  42257  dochnoncon  42264  djhlsmcl  42287  dihjat1lem  42301  dochsatshp  42324  dochsatshpb  42325  dochshpsat  42327  dochexmidlem2  42334  dochexmidlem5  42337  dochexmidlem6  42338  dochexmidlem7  42339  dochexmidlem8  42340  lclkrlem2p  42395  lclkrlem2v  42401  lcfrlem5  42419  lcfr  42458  mapdpglem17N  42561  mapdpglem18  42562  mapdpglem21  42565  islssfg  43911  islssfg2  43912  lnmlsslnm  43922  kercvrlsm  43924  lnmepi  43926  filnm  43931  gsumlsscl  49310  lincellss  49356  ellcoellss  49365