Theorem lssss 18985

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

Syntax hints:   → wi 4   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941   ⊆ wss 3607  ∅c0 3948  ‘cfv 5926  (class class class)co 6690  Basecbs 15904  +_gcplusg 15988  Scalarcsca 15991   ·_𝑠 cvsca 15992  LSubSpclss 18980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-iota 5889  df-fun 5928  df-fv 5934  df-ov 6693  df-lss 18981

This theorem is referenced by:  lssel  18986  lssuni  18988  00lss  18990  lsssubg  19005  islss3  19007  lsslss  19009  lssintcl  19012  lssmre  19014  lssacs  19015  lspid  19030  lspssv  19031  lspssp  19036  lsslsp  19063  lmhmima  19095  reslmhm  19100  lsmsp  19134  pj1lmhm  19148  lsppratlem2  19196  lsppratlem3  19197  lsppratlem4  19198  lspprat  19201  lbsextlem3  19208  lidlss  19258  ocvin  20066  pjdm2  20103  pjff  20104  pjf2  20106  pjfo  20107  pjcss  20108  frlmgsum  20159  frlmsplit2  20160  lsslindf  20217  lsslinds  20218  lssbn  23194  minveclem1  23241  minveclem2  23243  minveclem3a  23244  minveclem3b  23245  minveclem3  23246  minveclem4a  23247  minveclem4b  23248  minveclem4  23249  minveclem6  23251  minveclem7  23252  pjthlem1  23254  pjthlem2  23255  pjth  23256  islshpsm  34585  lshpnelb  34589  lshpnel2N  34590  lshpcmp  34593  lsatssv  34603  lssats  34617  lpssat  34618  lssatle  34620  lssat  34621  islshpcv  34658  lkrssv  34701  lkrlsp  34707  dvhopellsm  36723  dvadiaN  36734  dihss  36857  dihrnss  36884  dochord2N  36977  dochord3  36978  dihoml4  36983  dochsat  36989  dochshpncl  36990  dochnoncon  36997  djhlsmcl  37020  dihjat1lem  37034  dochsatshp  37057  dochsatshpb  37058  dochshpsat  37060  dochexmidlem2  37067  dochexmidlem5  37070  dochexmidlem6  37071  dochexmidlem7  37072  dochexmidlem8  37073  lclkrlem2p  37128  lclkrlem2v  37134  lcfrlem5  37152  lcfr  37191  mapdpglem17N  37294  mapdpglem18  37295  mapdpglem21  37298  islssfg  37957  islssfg2  37958  lnmlsslnm  37968  kercvrlsm  37970  lnmepi  37972  filnm  37977  gsumlsscl  42489  lincellss  42540  ellcoellss  42549