Theorem lssss 20207

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   ≠ wne 2944  ∀wral 3065   ⊆ wss 3888  ∅c0 4257  ‘cfv 6437  (class class class)co 7284  Basecbs 16921  +_gcplusg 16971  Scalarcsca 16974   ·_𝑠 cvsca 16975  LSubSpclss 20202

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 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6395  df-fun 6439  df-fv 6445  df-ov 7287  df-lss 20203

This theorem is referenced by:  lssel  20208  lssuni  20210  00lss  20212  lsssubg  20228  islss3  20230  lsslss  20232  lssintcl  20235  lssmre  20237  lssacs  20238  lspid  20253  lspssv  20254  lspssp  20259  lsslsp  20286  lmhmima  20318  reslmhm  20323  lsmsp  20357  pj1lmhm  20371  lsppratlem2  20419  lsppratlem3  20420  lsppratlem4  20421  lspprat  20424  lbsextlem3  20431  lidlss  20490  ocvin  20888  pjdm2  20927  pjff  20928  pjf2  20930  pjfo  20931  pjcss  20932  frlmgsum  20988  frlmsplit2  20989  lsslindf  21046  lsslinds  21047  cphsscph  24424  lssbn  24525  minveclem1  24597  minveclem2  24599  minveclem3a  24600  minveclem3b  24601  minveclem3  24602  minveclem4a  24603  minveclem4b  24604  minveclem4  24605  minveclem6  24607  minveclem7  24608  pjthlem1  24610  pjthlem2  24611  pjth  24612  lssdimle  31700  islshpsm  37001  lshpnelb  37005  lshpnel2N  37006  lshpcmp  37009  lsatssv  37019  lssats  37033  lpssat  37034  lssatle  37036  lssat  37037  islshpcv  37074  lkrssv  37117  lkrlsp  37123  dvhopellsm  39138  dvadiaN  39149  dihss  39272  dihrnss  39299  dochord2N  39392  dochord3  39393  dihoml4  39398  dochsat  39404  dochshpncl  39405  dochnoncon  39412  djhlsmcl  39435  dihjat1lem  39449  dochsatshp  39472  dochsatshpb  39473  dochshpsat  39475  dochexmidlem2  39482  dochexmidlem5  39485  dochexmidlem6  39486  dochexmidlem7  39487  dochexmidlem8  39488  lclkrlem2p  39543  lclkrlem2v  39549  lcfrlem5  39567  lcfr  39606  mapdpglem17N  39709  mapdpglem18  39710  mapdpglem21  39713  islssfg  40902  islssfg2  40903  lnmlsslnm  40913  kercvrlsm  40915  lnmepi  40917  filnm  40922  gsumlsscl  45730  lincellss  45778  ellcoellss  45787