Users' Mathboxes 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  v of a vector space  x is a vector space that has the same scalar set than 
x, whose addition and whose multiplication are restrictions of those of  x. (Contributed by FL, 30-Dec-2010.)
Assertion
Ref Expression
df-svs  |-  SubVec  =  ( x  e.  Vec  |->  { v  e.  Vec  | 
( ( 1st `  v
)  =  ( 1st `  x )  /\  ( 1st `  ( 2nd `  v
) )  C_  ( 1st `  ( 2nd `  x
) )  /\  ( 2nd `  ( 2nd `  v
) )  =  ( ( 2nd `  ( 2nd `  x ) )  |`  ( ran  ( 1st `  ( 1st `  x
) )  X.  ran  ( 1st `  ( 2nd `  v ) ) ) ) ) } )
Distinct variable group:    x, v

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