Theorem lssss 21262

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080   ⊆ wss 3900  ∅c0 4281  ‘cfv 6566  (class class class)co 7451  Basecbs 17431  +_gcplusg 17472  Scalarcsca 17475   ·_𝑠 cvsca 17476  LSubSpclss 21257

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-iota 6520  df-fun 6568  df-fv 6574  df-ov 7454  df-lss 21258

This theorem is used by:  lssel  21263  lssuni  21265  00lss  21267  lsssubg  21283  islss3  21285  lsslss  21287  lssintcl  21290  lssmre  21292  lssacs  21293  lspid  21308  lspssv  21309  lspssp  21314  lsslsp  21341  lmhmima  21373  reslmhm  21378  lsmsp  21412  pj1lmhm  21426  lsppratlem2  21477  lsppratlem3  21478  lsppratlem4  21479  lspprat  21482  lbsextlem3  21489  lidlss  21541  ocvin  22035  pjdm2  22072  pjff  22073  pjf2  22075  pjfo  22076  pjcss  22077  frlmgsum  22133  frlmsplit2  22134  lsslindf  22191  lsslinds  22192  cphsscph  25627  lssbn  25728  minveclem1  25800  minveclem2  25802  minveclem3a  25803  minveclem3b  25804  minveclem3  25805  minveclem4a  25806  minveclem4b  25807  minveclem4  25808  minveclem6  25810  minveclem7  25811  pjthlem1  25813  pjthlem2  25814  pjth  25815  lssdimle  34351  ply1degltdimlem  34365  ply1degltdim  34366  dimlssid  34375  islshpsm  40303  lshpnelb  40307  lshpnel2N  40308  lshpcmp  40311  lsatssv  40321  lssats  40335  lpssat  40336  lssatle  40338  lssat  40339  islshpcv  40376  lkrssv  40419  lkrlsp  40425  dvhopellsm  42440  dvadiaN  42451  dihss  42574  dihrnss  42601  dochord2N  42694  dochord3  42695  dihoml4  42700  dochsat  42706  dochshpncl  42707  dochnoncon  42714  djhlsmcl  42737  dihjat1lem  42751  dochsatshp  42774  dochsatshpb  42775  dochshpsat  42777  dochexmidlem2  42784  dochexmidlem5  42787  dochexmidlem6  42788  dochexmidlem7  42789  dochexmidlem8  42790  lclkrlem2p  42845  lclkrlem2v  42851  lcfrlem5  42869  lcfr  42908  mapdpglem17N  43011  mapdpglem18  43012  mapdpglem21  43015  islssfg  44338  islssfg2  44339  lnmlsslnm  44349  kercvrlsm  44351  lnmepi  44353  filnm  44358  gsumlsscl  49823  lincellss  49869  ellcoellss  49878