Theorem lssss 21086

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∀wral 3081   ⊆ wss 3906  ∅c0 4286  ‘cfv 6540  (class class class)co 7416  Basecbs 17286  +_gcplusg 17327  Scalarcsca 17330   ·_𝑠 cvsca 17331  LSubSpclss 21081

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fv 6548  df-ov 7419  df-lss 21082

This theorem is used by:  lssel  21087  lssuni  21089  00lss  21091  lsssubg  21107  islss3  21109  lsslss  21111  lssintcl  21114  lssmre  21116  lssacs  21117  lspid  21132  lspssv  21133  lspssp  21138  lsslsp  21165  lmhmima  21197  reslmhm  21202  lsmsp  21236  pj1lmhm  21250  lsppratlem2  21301  lsppratlem3  21302  lsppratlem4  21303  lspprat  21306  lbsextlem3  21313  lidlss  21365  ocvin  21853  pjdm2  21890  pjff  21891  pjf2  21893  pjfo  21894  pjcss  21895  frlmgsum  21951  frlmsplit2  21952  lsslindf  22009  lsslinds  22010  cphsscph  25439  lssbn  25540  minveclem1  25612  minveclem2  25614  minveclem3a  25615  minveclem3b  25616  minveclem3  25617  minveclem4a  25618  minveclem4b  25619  minveclem4  25620  minveclem6  25622  minveclem7  25623  pjthlem1  25625  pjthlem2  25626  pjth  25627  lssdimle  34021  ply1degltdimlem  34035  ply1degltdim  34036  dimlssid  34045  islshpsm  39787  lshpnelb  39791  lshpnel2N  39792  lshpcmp  39795  lsatssv  39805  lssats  39819  lpssat  39820  lssatle  39822  lssat  39823  islshpcv  39860  lkrssv  39903  lkrlsp  39909  dvhopellsm  41924  dvadiaN  41935  dihss  42058  dihrnss  42085  dochord2N  42178  dochord3  42179  dihoml4  42184  dochsat  42190  dochshpncl  42191  dochnoncon  42198  djhlsmcl  42221  dihjat1lem  42235  dochsatshp  42258  dochsatshpb  42259  dochshpsat  42261  dochexmidlem2  42268  dochexmidlem5  42271  dochexmidlem6  42272  dochexmidlem7  42273  dochexmidlem8  42274  lclkrlem2p  42329  lclkrlem2v  42335  lcfrlem5  42353  lcfr  42392  mapdpglem17N  42495  mapdpglem18  42496  mapdpglem21  42499  islssfg  43830  islssfg2  43831  lnmlsslnm  43841  kercvrlsm  43843  lnmepi  43845  filnm  43850  gsumlsscl  49193  lincellss  49239  ellcoellss  49248