Theorem lssss 20819

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099   ≠ wne 2937  ∀wral 3058   ⊆ wss 3947  ∅c0 4323  ‘cfv 6548  (class class class)co 7420  Basecbs 17179  +_gcplusg 17232  Scalarcsca 17235   ·_𝑠 cvsca 17236  LSubSpclss 20814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-iota 6500  df-fun 6550  df-fv 6556  df-ov 7423  df-lss 20815

This theorem is referenced by:  lssel  20820  lssuni  20822  00lss  20824  lsssubg  20840  islss3  20842  lsslss  20844  lssintcl  20847  lssmre  20849  lssacs  20850  lspid  20865  lspssv  20866  lspssp  20871  lsslsp  20898  lsslspOLD  20899  lmhmima  20931  reslmhm  20936  lsmsp  20970  pj1lmhm  20984  lsppratlem2  21035  lsppratlem3  21036  lsppratlem4  21037  lspprat  21040  lbsextlem3  21047  lidlss  21107  ocvin  21605  pjdm2  21644  pjff  21645  pjf2  21647  pjfo  21648  pjcss  21649  frlmgsum  21705  frlmsplit2  21706  lsslindf  21763  lsslinds  21764  cphsscph  25178  lssbn  25279  minveclem1  25351  minveclem2  25353  minveclem3a  25354  minveclem3b  25355  minveclem3  25356  minveclem4a  25357  minveclem4b  25358  minveclem4  25359  minveclem6  25361  minveclem7  25362  pjthlem1  25364  pjthlem2  25365  pjth  25366  lssdimle  33301  ply1degltdimlem  33316  ply1degltdim  33317  islshpsm  38452  lshpnelb  38456  lshpnel2N  38457  lshpcmp  38460  lsatssv  38470  lssats  38484  lpssat  38485  lssatle  38487  lssat  38488  islshpcv  38525  lkrssv  38568  lkrlsp  38574  dvhopellsm  40590  dvadiaN  40601  dihss  40724  dihrnss  40751  dochord2N  40844  dochord3  40845  dihoml4  40850  dochsat  40856  dochshpncl  40857  dochnoncon  40864  djhlsmcl  40887  dihjat1lem  40901  dochsatshp  40924  dochsatshpb  40925  dochshpsat  40927  dochexmidlem2  40934  dochexmidlem5  40937  dochexmidlem6  40938  dochexmidlem7  40939  dochexmidlem8  40940  lclkrlem2p  40995  lclkrlem2v  41001  lcfrlem5  41019  lcfr  41058  mapdpglem17N  41161  mapdpglem18  41162  mapdpglem21  41165  islssfg  42494  islssfg2  42495  lnmlsslnm  42505  kercvrlsm  42507  lnmepi  42509  filnm  42514  gsumlsscl  47447  lincellss  47494  ellcoellss  47503

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »