Metamath Proof Explorer


Definition df-lcv

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 ( 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 for binary relation. ( df-cv analog.) (Contributed by NM, 7-Jan-2015)

Ref Expression
Assertion df-lcv
|- 
    { <. t , u >. | ( ( t e. ( LSubSp ` w ) /\ u e. ( LSubSp ` w ) ) /\ ( t C. u /\ -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clcv
 |-  
1 vw
 |-  w
2 cvv
 |-  _V
3 vt
 |-  t
4 vu
 |-  u
5 3 cv
 |-  t
6 clss
 |-  LSubSp
7 1 cv
 |-  w
8 7 6 cfv
 |-  ( LSubSp ` w )
9 5 8 wcel
 |-  t e. ( LSubSp ` w )
10 4 cv
 |-  u
11 10 8 wcel
 |-  u e. ( LSubSp ` w )
12 9 11 wa
 |-  ( t e. ( LSubSp ` w ) /\ u e. ( LSubSp ` w ) )
13 5 10 wpss
 |-  t C. u
14 vs
 |-  s
15 14 cv
 |-  s
16 5 15 wpss
 |-  t C. s
17 15 10 wpss
 |-  s C. u
18 16 17 wa
 |-  ( t C. s /\ s C. u )
19 18 14 8 wrex
 |-  E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u )
20 19 wn
 |-  -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u )
21 13 20 wa
 |-  ( t C. u /\ -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) )
22 12 21 wa
 |-  ( ( t e. ( LSubSp ` w ) /\ u e. ( LSubSp ` w ) ) /\ ( t C. u /\ -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) ) )
23 22 3 4 copab
 |-  { <. t , u >. | ( ( t e. ( LSubSp ` w ) /\ u e. ( LSubSp ` w ) ) /\ ( t C. u /\ -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) ) ) }
24 1 2 23 cmpt
 |-  ( 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 ) ) ) } )
25 0 24 wceq
 |-  
    { <. t , u >. | ( ( t e. ( LSubSp ` w ) /\ u e. ( LSubSp ` w ) ) /\ ( t C. u /\ -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) ) ) } )