Theorem lssss 21038

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 21036	. 2 ⊢ (𝑈 ∈ 𝑆 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥( ·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑈))
8	7	simp1bi 1163	1 ⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079   ⊆ wss 3906  ∅c0 4287  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  +_gcplusg 17311  Scalarcsca 17314   ·_𝑠 cvsca 17315  LSubSpclss 21033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7415  df-lss 21034

This theorem is referenced by:  lssel  21039  lssuni  21041  00lss  21043  lsssubg  21059  islss3  21061  lsslss  21063  lssintcl  21066  lssmre  21068  lssacs  21069  lspid  21084  lspssv  21085  lspssp  21090  lsslsp  21117  lmhmima  21149  reslmhm  21154  lsmsp  21188  pj1lmhm  21202  lsppratlem2  21253  lsppratlem3  21254  lsppratlem4  21255  lspprat  21258  lbsextlem3  21265  lidlss  21317  ocvin  21805  pjdm2  21842  pjff  21843  pjf2  21845  pjfo  21846  pjcss  21847  frlmgsum  21903  frlmsplit2  21904  lsslindf  21961  lsslinds  21962  cphsscph  25391  lssbn  25492  minveclem1  25564  minveclem2  25566  minveclem3a  25567  minveclem3b  25568  minveclem3  25569  minveclem4a  25570  minveclem4b  25571  minveclem4  25572  minveclem6  25574  minveclem7  25575  pjthlem1  25577  pjthlem2  25578  pjth  25579  lssdimle  33979  ply1degltdimlem  33993  ply1degltdim  33994  dimlssid  34003  islshpsm  39735  lshpnelb  39739  lshpnel2N  39740  lshpcmp  39743  lsatssv  39753  lssats  39767  lpssat  39768  lssatle  39770  lssat  39771  islshpcv  39808  lkrssv  39851  lkrlsp  39857  dvhopellsm  41872  dvadiaN  41883  dihss  42006  dihrnss  42033  dochord2N  42126  dochord3  42127  dihoml4  42132  dochsat  42138  dochshpncl  42139  dochnoncon  42146  djhlsmcl  42169  dihjat1lem  42183  dochsatshp  42206  dochsatshpb  42207  dochshpsat  42209  dochexmidlem2  42216  dochexmidlem5  42219  dochexmidlem6  42220  dochexmidlem7  42221  dochexmidlem8  42222  lclkrlem2p  42277  lclkrlem2v  42283  lcfrlem5  42301  lcfr  42340  mapdpglem17N  42443  mapdpglem18  42444  mapdpglem21  42447  islssfg  43780  islssfg2  43781  lnmlsslnm  43791  kercvrlsm  43793  lnmepi  43795  filnm  43800  gsumlsscl  49143  lincellss  49189  ellcoellss  49198