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

Metamath Proof Explorer

Theorem lcvntr

Description: The covers relation is not transitive. ( cvntr analog.) (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lcvnbtwn.s 
|- S = ( LSubSp ` W )
lcvnbtwn.c 
|- C = (
    lcvnbtwn.w 
    |- ( ph -> W e. X )
    lcvnbtwn.r 
    |- ( ph -> R e. S )
    lcvnbtwn.t 
    |- ( ph -> T e. S )
    lcvnbtwn.u 
    |- ( ph -> U e. S )
    lcvnbtwn.d 
    |- ( ph -> R C T )
    lcvntr.p 
    |- ( ph -> T C U )
    Assertion lcvntr 
    |- ( ph -> -. R C U )

    Proof

    Step Hyp Ref Expression
    1 lcvnbtwn.s 
     |-  S = ( LSubSp ` W )
    2 lcvnbtwn.c 
     |-  C = (
      3 lcvnbtwn.w 
       |-  ( ph -> W e. X )
      4 lcvnbtwn.r 
       |-  ( ph -> R e. S )
      5 lcvnbtwn.t 
       |-  ( ph -> T e. S )
      6 lcvnbtwn.u 
       |-  ( ph -> U e. S )
      7 lcvnbtwn.d 
       |-  ( ph -> R C T )
      8 lcvntr.p 
       |-  ( ph -> T C U )
      9 1 2 3 4 5 7 lcvpss 
       |-  ( ph -> R C. T )
      10 1 2 3 5 6 8 lcvpss 
       |-  ( ph -> T C. U )
      11 9 10 jca 
       |-  ( ph -> ( R C. T /\ T C. U ) )
      12 3 adantr 
       |-  ( ( ph /\ R C U ) -> W e. X )
      13 4 adantr 
       |-  ( ( ph /\ R C U ) -> R e. S )
      14 6 adantr 
       |-  ( ( ph /\ R C U ) -> U e. S )
      15 5 adantr 
       |-  ( ( ph /\ R C U ) -> T e. S )
      16 simpr 
       |-  ( ( ph /\ R C U ) -> R C U )
      17 1 2 12 13 14 15 16 lcvnbtwn 
       |-  ( ( ph /\ R C U ) -> -. ( R C. T /\ T C. U ) )
      18 17 ex 
       |-  ( ph -> ( R C U -> -. ( R C. T /\ T C. U ) ) )
      19 11 18 mt2d 
       |-  ( ph -> -. R C U )