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 )