Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-svs Unicode version

Definition df-svs 25486
 Description: A sub-vector space of a vector space is a vector space that has the same scalar set than , whose addition and whose multiplication are restrictions of those of . (Contributed by FL, 30-Dec-2010.)
Assertion
Ref Expression
df-svs
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-svs
StepHypRef Expression
1 csvec 25485 . 2
2 vx . . 3
3 cvec 25449 . . 3
4 vv . . . . . . . 8
54cv 1622 . . . . . . 7
6 c1st 6120 . . . . . . 7
75, 6cfv 5255 . . . . . 6
82cv 1622 . . . . . . 7
98, 6cfv 5255 . . . . . 6
107, 9wceq 1623 . . . . 5
11 c2nd 6121 . . . . . . . 8
125, 11cfv 5255 . . . . . . 7
1312, 6cfv 5255 . . . . . 6
148, 11cfv 5255 . . . . . . 7
1514, 6cfv 5255 . . . . . 6
1613, 15wss 3152 . . . . 5
1712, 11cfv 5255 . . . . . 6
1814, 11cfv 5255 . . . . . . 7
199, 6cfv 5255 . . . . . . . . 9
2019crn 4690 . . . . . . . 8
2113crn 4690 . . . . . . . 8
2220, 21cxp 4687 . . . . . . 7
2318, 22cres 4691 . . . . . 6
2417, 23wceq 1623 . . . . 5
2510, 16, 24w3a 934 . . . 4
2625, 4, 3crab 2547 . . 3
272, 3, 26cmpt 4077 . 2
281, 27wceq 1623 1
 Colors of variables: wff set class This definition is referenced by:  svs2  25487  svs3  25488
 Copyright terms: Public domain W3C validator