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

Metamath Proof Explorer

Theorem cdlemg5

Description: TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle ? TODO: The .\/ hypothesis is unused. FIX COMMENT. (Contributed by NM, 26-Apr-2013)

Ref Expression
Hypotheses cdlemg5.l 
|- .<_ = ( le ` K )
cdlemg5.j 
|- .\/ = ( join ` K )
cdlemg5.a 
|- A = ( Atoms ` K )
cdlemg5.h 
|- H = ( LHyp ` K )
Assertion cdlemg5 
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> E. q e. A ( P =/= q /\ -. q .<_ W ) )

Proof

Step Hyp Ref Expression
1 cdlemg5.l 
 |-  .<_ = ( le ` K )
2 cdlemg5.j 
 |-  .\/ = ( join ` K )
3 cdlemg5.a 
 |-  A = ( Atoms ` K )
4 cdlemg5.h 
 |-  H = ( LHyp ` K )
5 1 3 4 lhpexle 
 |-  ( ( K e. HL /\ W e. H ) -> E. r e. A r .<_ W )
6 5 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> E. r e. A r .<_ W )
7 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( r e. A /\ r .<_ W ) ) -> ( K e. HL /\ W e. H ) )
8 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( r e. A /\ r .<_ W ) ) -> ( r e. A /\ r .<_ W ) )
9 simplr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( r e. A /\ r .<_ W ) ) -> ( P e. A /\ -. P .<_ W ) )
10 1 2 3 4 cdlemf1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( r e. A /\ r .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> E. q e. A ( P =/= q /\ -. q .<_ W /\ r .<_ ( P .\/ q ) ) )
11 7 8 9 10 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( r e. A /\ r .<_ W ) ) -> E. q e. A ( P =/= q /\ -. q .<_ W /\ r .<_ ( P .\/ q ) ) )
12 3simpa 
 |-  ( ( P =/= q /\ -. q .<_ W /\ r .<_ ( P .\/ q ) ) -> ( P =/= q /\ -. q .<_ W ) )
13 12 reximi 
 |-  ( E. q e. A ( P =/= q /\ -. q .<_ W /\ r .<_ ( P .\/ q ) ) -> E. q e. A ( P =/= q /\ -. q .<_ W ) )
14 11 13 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( r e. A /\ r .<_ W ) ) -> E. q e. A ( P =/= q /\ -. q .<_ W ) )
15 6 14 rexlimddv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> E. q e. A ( P =/= q /\ -. q .<_ W ) )