Metamath Proof Explorer

Theorem atbtwnex

Description: Given atoms P in X and Q not in X , there exists an atom r not in X such that the line Q .\/ r intersects X at P . (Contributed by NM, 1-Aug-2012)

Ref Expression
Hypotheses atbtwn.b 
|- B = ( Base ` K )
atbtwn.l 
|- .<_ = ( le ` K )
atbtwn.j 
|- .\/ = ( join ` K )
atbtwn.a 
|- A = ( Atoms ` K )
Assertion atbtwnex 
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) -> E. r e. A ( r =/= Q /\ -. r .<_ X /\ P .<_ ( Q .\/ r ) ) )

Proof

Step Hyp Ref Expression
1 atbtwn.b 
 |-  B = ( Base ` K )
2 atbtwn.l 
 |-  .<_ = ( le ` K )
3 atbtwn.j 
 |-  .\/ = ( join ` K )
4 atbtwn.a 
 |-  A = ( Atoms ` K )
5 simpr2 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) -> P .<_ X )
6 simpr3 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) -> -. Q .<_ X )
7 nbrne2 
 |-  ( ( P .<_ X /\ -. Q .<_ X ) -> P =/= Q )
8 5 6 7 syl2anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) -> P =/= Q )
9 2 3 4 hlsupr 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> E. r e. A ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) )
10 8 9 syldan 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) -> E. r e. A ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) )
11 simp32 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> r =/= Q )
12 simp31 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> r =/= P )
13 simp1l 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
14 simp2 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> r e. A )
15 simp1r1 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> X e. B )
16 simp1r2 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> P .<_ X )
17 simp1r3 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> -. Q .<_ X )
18 simp33 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> r .<_ ( P .\/ Q ) )
19 1 2 3 4 atbtwn 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( r e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ r .<_ ( P .\/ Q ) ) ) -> ( r =/= P <-> -. r .<_ X ) )
20 13 14 15 16 17 18 19 syl123anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> ( r =/= P <-> -. r .<_ X ) )
21 12 20 mpbid 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> -. r .<_ X )
22 simp1l1 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> K e. HL )
23 simp1l2 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> P e. A )
24 simp1l3 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> Q e. A )
25 2 3 4 hlatexch2 
 |-  ( ( K e. HL /\ ( r e. A /\ P e. A /\ Q e. A ) /\ r =/= Q ) -> ( r .<_ ( P .\/ Q ) -> P .<_ ( r .\/ Q ) ) )
26 22 14 23 24 11 25 syl131anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> ( r .<_ ( P .\/ Q ) -> P .<_ ( r .\/ Q ) ) )
27 18 26 mpd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> P .<_ ( r .\/ Q ) )
28 3 4 hlatjcom 
 |-  ( ( K e. HL /\ Q e. A /\ r e. A ) -> ( Q .\/ r ) = ( r .\/ Q ) )
29 22 24 14 28 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> ( Q .\/ r ) = ( r .\/ Q ) )
30 27 29 breqtrrd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> P .<_ ( Q .\/ r ) )
31 11 21 30 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) /\ r e. A /\ ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) -> ( r =/= Q /\ -. r .<_ X /\ P .<_ ( Q .\/ r ) ) )
32 31 3exp 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) -> ( r e. A -> ( ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) -> ( r =/= Q /\ -. r .<_ X /\ P .<_ ( Q .\/ r ) ) ) ) )
33 32 reximdvai 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) -> ( E. r e. A ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) -> E. r e. A ( r =/= Q /\ -. r .<_ X /\ P .<_ ( Q .\/ r ) ) ) )
34 10 33 mpd 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P .<_ X /\ -. Q .<_ X ) ) -> E. r e. A ( r =/= Q /\ -. r .<_ X /\ P .<_ ( Q .\/ r ) ) )