Metamath Proof Explorer

Theorem atbtwn

Description: Property of a 3rd atom R on a line P .\/ Q intersecting element X at P . (Contributed by NM, 30-Jul-2012)

Ref Expression
Hypotheses atbtwn.b 
|- B = ( Base ` K )
atbtwn.l 
|- .<_ = ( le ` K )
atbtwn.j 
|- .\/ = ( join ` K )
atbtwn.a 
|- A = ( Atoms ` K )
Assertion 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 ) )

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 simpl33 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> R .<_ ( P .\/ Q ) )
6 simpr 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> R .<_ X )
7 simpl11 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> K e. HL )
8 7 hllatd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> K e. Lat )
9 simpl2l 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> R e. A )
10 1 4 atbase 
 |-  ( R e. A -> R e. B )
11 9 10 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> R e. B )
12 simpl1 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
13 1 3 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. B )
14 12 13 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> ( P .\/ Q ) e. B )
15 simpl2r 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> X e. B )
16 eqid 
 |-  ( meet ` K ) = ( meet ` K )
17 1 2 16 latlem12 
 |-  ( ( K e. Lat /\ ( R e. B /\ ( P .\/ Q ) e. B /\ X e. B ) ) -> ( ( R .<_ ( P .\/ Q ) /\ R .<_ X ) <-> R .<_ ( ( P .\/ Q ) ( meet ` K ) X ) ) )
18 8 11 14 15 17 syl13anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> ( ( R .<_ ( P .\/ Q ) /\ R .<_ X ) <-> R .<_ ( ( P .\/ Q ) ( meet ` K ) X ) ) )
19 5 6 18 mpbi2and 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> R .<_ ( ( P .\/ Q ) ( meet ` K ) X ) )
20 simpl12 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> P e. A )
21 simpl13 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> Q e. A )
22 simpl31 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> P .<_ X )
23 simpl32 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> -. Q .<_ X )
24 1 2 3 16 4 2atjm 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X ) ) -> ( ( P .\/ Q ) ( meet ` K ) X ) = P )
25 7 20 21 15 22 23 24 syl132anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> ( ( P .\/ Q ) ( meet ` K ) X ) = P )
26 19 25 breqtrd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> R .<_ P )
27 hlatl 
 |-  ( K e. HL -> K e. AtLat )
28 7 27 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> K e. AtLat )
29 2 4 atcmp 
 |-  ( ( K e. AtLat /\ R e. A /\ P e. A ) -> ( R .<_ P <-> R = P ) )
30 28 9 20 29 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> ( R .<_ P <-> R = P ) )
31 26 30 mpbid 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R .<_ X ) -> R = P )
32 31 ex 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) -> ( R .<_ X -> R = P ) )
33 32 necon3ad 
 |-  ( ( ( 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 ) )
34 simp31 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) -> P .<_ X )
35 nbrne2 
 |-  ( ( P .<_ X /\ -. R .<_ X ) -> P =/= R )
36 35 necomd 
 |-  ( ( P .<_ X /\ -. R .<_ X ) -> R =/= P )
37 36 ex 
 |-  ( P .<_ X -> ( -. R .<_ X -> R =/= P ) )
38 34 37 syl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ X e. B ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) -> ( -. R .<_ X -> R =/= P ) )
39 33 38 impbid 
 |-  ( ( ( 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 ) )