This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lcvbr2

Description: The covers relation for a left vector space (or a left module). ( cvbr2 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 lcvbr2 
    |- ( ph -> ( T C U <-> ( T C. U /\ A. s e. S ( ( T C. s /\ s C_ U ) -> s = 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 1 2 3 4 5 lcvbr 
       |-  ( ph -> ( T C U <-> ( T C. U /\ -. E. s e. S ( T C. s /\ s C. U ) ) ) )
      7 iman 
       |-  ( ( ( T C. s /\ s C_ U ) -> s = U ) <-> -. ( ( T C. s /\ s C_ U ) /\ -. s = U ) )
      8 anass 
       |-  ( ( ( T C. s /\ s C_ U ) /\ -. s = U ) <-> ( T C. s /\ ( s C_ U /\ -. s = U ) ) )
      9 dfpss2 
       |-  ( s C. U <-> ( s C_ U /\ -. s = U ) )
      10 9 anbi2i 
       |-  ( ( T C. s /\ s C. U ) <-> ( T C. s /\ ( s C_ U /\ -. s = U ) ) )
      11 8 10 bitr4i 
       |-  ( ( ( T C. s /\ s C_ U ) /\ -. s = U ) <-> ( T C. s /\ s C. U ) )
      12 7 11 xchbinx 
       |-  ( ( ( T C. s /\ s C_ U ) -> s = U ) <-> -. ( T C. s /\ s C. U ) )
      13 12 ralbii 
       |-  ( A. s e. S ( ( T C. s /\ s C_ U ) -> s = U ) <-> A. s e. S -. ( T C. s /\ s C. U ) )
      14 ralnex 
       |-  ( A. s e. S -. ( T C. s /\ s C. U ) <-> -. E. s e. S ( T C. s /\ s C. U ) )
      15 13 14 bitri 
       |-  ( A. s e. S ( ( T C. s /\ s C_ U ) -> s = U ) <-> -. E. s e. S ( T C. s /\ s C. U ) )
      16 15 anbi2i 
       |-  ( ( T C. U /\ A. s e. S ( ( T C. s /\ s C_ U ) -> s = U ) ) <-> ( T C. U /\ -. E. s e. S ( T C. s /\ s C. U ) ) )
      17 6 16 bitr4di 
       |-  ( ph -> ( T C U <-> ( T C. U /\ A. s e. S ( ( T C. s /\ s C_ U ) -> s = U ) ) ) )