Metamath Proof Explorer

Theorem lcvfbr

Description: The covers relation for a left vector space (or a left module). (Contributed by NM, 7-Jan-2015)

Ref Expression
Hypotheses lcvfbr.s 
|- S = ( LSubSp ` W )
lcvfbr.c 
|- C = (
    lcvfbr.w 
    |- ( ph -> W e. X )
    Assertion lcvfbr 
    |- ( ph -> C = { <. t , u >. | ( ( t e. S /\ u e. S ) /\ ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) ) } )

    Proof

    Step Hyp Ref Expression
    1 lcvfbr.s 
     |-  S = ( LSubSp ` W )
    2 lcvfbr.c 
     |-  C = (
      3 lcvfbr.w 
       |-  ( ph -> W e. X )
      4 elex 
       |-  ( W e. X -> W e. _V )
      5 fveq2 
       |-  ( w = W -> ( LSubSp ` w ) = ( LSubSp ` W ) )
      6 5 1 eqtr4di 
       |-  ( w = W -> ( LSubSp ` w ) = S )
      7 6 eleq2d 
       |-  ( w = W -> ( t e. ( LSubSp ` w ) <-> t e. S ) )
      8 6 eleq2d 
       |-  ( w = W -> ( u e. ( LSubSp ` w ) <-> u e. S ) )
      9 7 8 anbi12d 
       |-  ( w = W -> ( ( t e. ( LSubSp ` w ) /\ u e. ( LSubSp ` w ) ) <-> ( t e. S /\ u e. S ) ) )
      10 6 rexeqdv 
       |-  ( w = W -> ( E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) <-> E. s e. S ( t C. s /\ s C. u ) ) )
      11 10 notbid 
       |-  ( w = W -> ( -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) <-> -. E. s e. S ( t C. s /\ s C. u ) ) )
      12 11 anbi2d 
       |-  ( w = W -> ( ( t C. u /\ -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) ) <-> ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) ) )
      13 9 12 anbi12d 
       |-  ( w = W -> ( ( ( t e. ( LSubSp ` w ) /\ u e. ( LSubSp ` w ) ) /\ ( t C. u /\ -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) ) ) <-> ( ( t e. S /\ u e. S ) /\ ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) ) ) )
      14 13 opabbidv 
       |-  ( w = W -> { <. t , u >. | ( ( t e. ( LSubSp ` w ) /\ u e. ( LSubSp ` w ) ) /\ ( t C. u /\ -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) ) ) } = { <. t , u >. | ( ( t e. S /\ u e. S ) /\ ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) ) } )
      15 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 ) ) ) } )
      16 1 fvexi 
       |-  S e. _V
      17 16 16 xpex 
       |-  ( S X. S ) e. _V
      18 opabssxp 
       |-  { <. t , u >. | ( ( t e. S /\ u e. S ) /\ ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) ) } C_ ( S X. S )
      19 17 18 ssexi 
       |-  { <. t , u >. | ( ( t e. S /\ u e. S ) /\ ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) ) } e. _V
      20 14 15 19 fvmpt 
       |-  ( W e. _V -> ( 
        . | ( ( t e. S /\ u e. S ) /\ ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) ) } )
      21 3 4 20 3syl 
       |-  ( ph -> ( 
        . | ( ( t e. S /\ u e. S ) /\ ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) ) } )
      22 2 21 syl5eq 
       |-  ( ph -> C = { <. t , u >. | ( ( t e. S /\ u e. S ) /\ ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) ) } )