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 ) ) ) } )