Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lcv Unicode version

Definition df-lcv 28376
Description: Define the covering relation for subspaces of a left vector space. Similar to Definition 3.2.18 of [PtakPulmannova] p. 68. Ptak/Pulmannova's notation 
A (  <oLL  `  W ) B is read " B covers  A " or " A is covered by  B " , and it means that  B is larger than  A and there is nothing in between. See lcvbr 28378 for binary relation. (df-cv 22819 analog.) (Contributed by NM, 7-Jan-2015.)
Assertion
Ref Expression
df-lcv  |-  <oLL  =  (
w  e.  _V  |->  {
<. t ,  u >.  |  ( ( t  e.  ( LSubSp `  w )  /\  u  e.  ( LSubSp `
 w ) )  /\  ( t  C.  u  /\  -.  E. s  e.  ( LSubSp `  w )
( t  C.  s  /\  s  C.  u ) ) ) } )
Distinct variable group:    t, s, u, w

Detailed syntax breakdown of Definition df-lcv
StepHypRef Expression
1 clcv 28375 . 2  class  <oLL
2 vw . . 3  set  w
3 cvv 2763 . . 3  class  _V
4 vt . . . . . . . 8  set  t
54cv 1618 . . . . . . 7  class  t
62cv 1618 . . . . . . . 8  class  w
7 clss 15651 . . . . . . . 8  class  LSubSp
86, 7cfv 4673 . . . . . . 7  class  ( LSubSp `  w )
95, 8wcel 1621 . . . . . 6  wff  t  e.  ( LSubSp `  w )
10 vu . . . . . . . 8  set  u
1110cv 1618 . . . . . . 7  class  u
1211, 8wcel 1621 . . . . . 6  wff  u  e.  ( LSubSp `  w )
139, 12wa 360 . . . . 5  wff  ( t  e.  ( LSubSp `  w
)  /\  u  e.  ( LSubSp `  w )
)
145, 11wpss 3128 . . . . . 6  wff  t  C.  u
15 vs . . . . . . . . . . 11  set  s
1615cv 1618 . . . . . . . . . 10  class  s
175, 16wpss 3128 . . . . . . . . 9  wff  t  C.  s
1816, 11wpss 3128 . . . . . . . . 9  wff  s  C.  u
1917, 18wa 360 . . . . . . . 8  wff  ( t 
C.  s  /\  s  C.  u )
2019, 15, 8wrex 2519 . . . . . . 7  wff  E. s  e.  ( LSubSp `  w )
( t  C.  s  /\  s  C.  u )
2120wn 5 . . . . . 6  wff  -.  E. s  e.  ( LSubSp `  w ) ( t 
C.  s  /\  s  C.  u )
2214, 21wa 360 . . . . 5  wff  ( t 
C.  u  /\  -.  E. s  e.  ( LSubSp `  w ) ( t 
C.  s  /\  s  C.  u ) )
2313, 22wa 360 . . . 4  wff  ( ( t  e.  ( LSubSp `  w )  /\  u  e.  ( LSubSp `  w )
)  /\  ( t  C.  u  /\  -.  E. s  e.  ( LSubSp `  w ) ( t 
C.  s  /\  s  C.  u ) ) )
2423, 4, 10copab 4050 . . 3  class  { <. t ,  u >.  |  ( ( t  e.  (
LSubSp `  w )  /\  u  e.  ( LSubSp `  w ) )  /\  ( t  C.  u  /\  -.  E. s  e.  ( LSubSp `  w )
( t  C.  s  /\  s  C.  u ) ) ) }
252, 3, 24cmpt 4051 . 2  class  ( w  e.  _V  |->  { <. t ,  u >.  |  ( ( t  e.  (
LSubSp `  w )  /\  u  e.  ( LSubSp `  w ) )  /\  ( t  C.  u  /\  -.  E. s  e.  ( LSubSp `  w )
( t  C.  s  /\  s  C.  u ) ) ) } )
261, 25wceq 1619 1  wff  <oLL  =  (
w  e.  _V  |->  {
<. t ,  u >.  |  ( ( t  e.  ( LSubSp `  w )  /\  u  e.  ( LSubSp `
 w ) )  /\  ( t  C.  u  /\  -.  E. s  e.  ( LSubSp `  w )
( t  C.  s  /\  s  C.  u ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  lcvfbr  28377
  Copyright terms: Public domain W3C validator