Metamath Proof Explorer

Theorem lcvbr3

Description: The covers relation for a left vector space (or a left module). (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 lcvbr3 
    |- ( ph -> ( T C U <-> ( T C. U /\ A. s e. S ( ( T C_ s /\ s C_ U ) -> ( s = T \/ 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 = T \/ s = U ) ) <-> -. ( ( T C_ s /\ s C_ U ) /\ -. ( s = T \/ s = U ) ) )
      8 df-pss 
       |-  ( T C. s <-> ( T C_ s /\ T =/= s ) )
      9 necom 
       |-  ( T =/= s <-> s =/= T )
      10 9 anbi2i 
       |-  ( ( T C_ s /\ T =/= s ) <-> ( T C_ s /\ s =/= T ) )
      11 8 10 bitri 
       |-  ( T C. s <-> ( T C_ s /\ s =/= T ) )
      12 df-pss 
       |-  ( s C. U <-> ( s C_ U /\ s =/= U ) )
      13 11 12 anbi12i 
       |-  ( ( T C. s /\ s C. U ) <-> ( ( T C_ s /\ s =/= T ) /\ ( s C_ U /\ s =/= U ) ) )
      14 an4 
       |-  ( ( ( T C_ s /\ s =/= T ) /\ ( s C_ U /\ s =/= U ) ) <-> ( ( T C_ s /\ s C_ U ) /\ ( s =/= T /\ s =/= U ) ) )
      15 neanior 
       |-  ( ( s =/= T /\ s =/= U ) <-> -. ( s = T \/ s = U ) )
      16 15 anbi2i 
       |-  ( ( ( T C_ s /\ s C_ U ) /\ ( s =/= T /\ s =/= U ) ) <-> ( ( T C_ s /\ s C_ U ) /\ -. ( s = T \/ s = U ) ) )
      17 14 16 bitri 
       |-  ( ( ( T C_ s /\ s =/= T ) /\ ( s C_ U /\ s =/= U ) ) <-> ( ( T C_ s /\ s C_ U ) /\ -. ( s = T \/ s = U ) ) )
      18 13 17 bitri 
       |-  ( ( T C. s /\ s C. U ) <-> ( ( T C_ s /\ s C_ U ) /\ -. ( s = T \/ s = U ) ) )
      19 7 18 xchbinxr 
       |-  ( ( ( T C_ s /\ s C_ U ) -> ( s = T \/ s = U ) ) <-> -. ( T C. s /\ s C. U ) )
      20 19 ralbii 
       |-  ( A. s e. S ( ( T C_ s /\ s C_ U ) -> ( s = T \/ s = U ) ) <-> A. s e. S -. ( T C. s /\ s C. U ) )
      21 ralnex 
       |-  ( A. s e. S -. ( T C. s /\ s C. U ) <-> -. E. s e. S ( T C. s /\ s C. U ) )
      22 20 21 bitri 
       |-  ( A. s e. S ( ( T C_ s /\ s C_ U ) -> ( s = T \/ s = U ) ) <-> -. E. s e. S ( T C. s /\ s C. U ) )
      23 22 anbi2i 
       |-  ( ( T C. U /\ A. s e. S ( ( T C_ s /\ s C_ U ) -> ( s = T \/ s = U ) ) ) <-> ( T C. U /\ -. E. s e. S ( T C. s /\ s C. U ) ) )
      24 6 23 bitr4di 
       |-  ( ph -> ( T C U <-> ( T C. U /\ A. s e. S ( ( T C_ s /\ s C_ U ) -> ( s = T \/ s = U ) ) ) ) )