Metamath Proof Explorer

Theorem lcvbr

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

Ref Expression
Hypotheses lcvfbr.s 
|- S = ( LSubSp ` W )
lcvfbr.c 
|- C = (
    lcvfbr.w 
    |- ( ph -> W e. X )
    lcvfbr.t 
    |- ( ph -> T e. S )
    lcvfbr.u 
    |- ( ph -> U e. S )
    Assertion lcvbr 
    |- ( ph -> ( T C U <-> ( 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 lcvfbr.t 
       |-  ( ph -> T e. S )
      5 lcvfbr.u 
       |-  ( ph -> U e. S )
      6 eleq1 
       |-  ( t = T -> ( t e. S <-> T e. S ) )
      7 6 anbi1d 
       |-  ( t = T -> ( ( t e. S /\ u e. S ) <-> ( T e. S /\ u e. S ) ) )
      8 psseq1 
       |-  ( t = T -> ( t C. u <-> T C. u ) )
      9 psseq1 
       |-  ( t = T -> ( t C. s <-> T C. s ) )
      10 9 anbi1d 
       |-  ( t = T -> ( ( t C. s /\ s C. u ) <-> ( T C. s /\ s C. u ) ) )
      11 10 rexbidv 
       |-  ( t = T -> ( E. s e. S ( t C. s /\ s C. u ) <-> E. s e. S ( T C. s /\ s C. u ) ) )
      12 11 notbid 
       |-  ( t = T -> ( -. E. s e. S ( t C. s /\ s C. u ) <-> -. E. s e. S ( T C. s /\ s C. u ) ) )
      13 8 12 anbi12d 
       |-  ( t = T -> ( ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) <-> ( T C. u /\ -. E. s e. S ( T C. s /\ s C. u ) ) ) )
      14 7 13 anbi12d 
       |-  ( t = T -> ( ( ( t e. S /\ u e. S ) /\ ( t C. u /\ -. E. s e. S ( 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 ) ) ) ) )
      15 eleq1 
       |-  ( u = U -> ( u e. S <-> U e. S ) )
      16 15 anbi2d 
       |-  ( u = U -> ( ( T e. S /\ u e. S ) <-> ( T e. S /\ U e. S ) ) )
      17 psseq2 
       |-  ( u = U -> ( T C. u <-> T C. U ) )
      18 psseq2 
       |-  ( u = U -> ( s C. u <-> s C. U ) )
      19 18 anbi2d 
       |-  ( u = U -> ( ( T C. s /\ s C. u ) <-> ( T C. s /\ s C. U ) ) )
      20 19 rexbidv 
       |-  ( u = U -> ( E. s e. S ( T C. s /\ s C. u ) <-> E. s e. S ( T C. s /\ s C. U ) ) )
      21 20 notbid 
       |-  ( u = U -> ( -. E. s e. S ( T C. s /\ s C. u ) <-> -. E. s e. S ( T C. s /\ s C. U ) ) )
      22 17 21 anbi12d 
       |-  ( u = U -> ( ( T C. u /\ -. E. s e. S ( T C. s /\ s C. u ) ) <-> ( T C. U /\ -. E. s e. S ( T C. s /\ s C. U ) ) ) )
      23 16 22 anbi12d 
       |-  ( u = U -> ( ( ( T e. S /\ u e. S ) /\ ( T C. u /\ -. E. s e. S ( 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 ) ) ) ) )
      24 eqid 
       |-  { <. t , u >. | ( ( t e. S /\ u e. S ) /\ ( t C. u /\ -. E. s e. S ( 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 ) ) ) }
      25 14 23 24 brabg 
       |-  ( ( T e. S /\ U e. S ) -> ( T { <. t , u >. | ( ( t e. S /\ u e. S ) /\ ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) ) } U <-> ( ( T e. S /\ U e. S ) /\ ( T C. U /\ -. E. s e. S ( T C. s /\ s C. U ) ) ) ) )
      26 4 5 25 syl2anc 
       |-  ( ph -> ( T { <. t , u >. | ( ( t e. S /\ u e. S ) /\ ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) ) } U <-> ( ( T e. S /\ U e. S ) /\ ( T C. U /\ -. E. s e. S ( T C. s /\ s C. U ) ) ) ) )
      27 1 2 3 lcvfbr 
       |-  ( ph -> C = { <. t , u >. | ( ( t e. S /\ u e. S ) /\ ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) ) } )
      28 27 breqd 
       |-  ( ph -> ( T C U <-> T { <. t , u >. | ( ( t e. S /\ u e. S ) /\ ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) ) } U ) )
      29 4 5 jca 
       |-  ( ph -> ( T e. S /\ U e. S ) )
      30 29 biantrurd 
       |-  ( ph -> ( ( T C. U /\ -. E. s e. S ( 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 ) ) ) ) )
      31 26 28 30 3bitr4d 
       |-  ( ph -> ( T C U <-> ( T C. U /\ -. E. s e. S ( T C. s /\ s C. U ) ) ) )