Metamath Proof Explorer

Theorem cdlema1N

Description: A condition for required for proof of Lemma A in Crawley p. 112. (Contributed by NM, 29-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdlema1.b 
|- B = ( Base ` K )
cdlema1.l 
|- .<_ = ( le ` K )
cdlema1.j 
|- .\/ = ( join ` K )
cdlema1.m 
|- ./\ = ( meet ` K )
cdlema1.a 
|- A = ( Atoms ` K )
cdlema1.n 
|- N = ( Lines ` K )
cdlema1.f 
|- F = ( pmap ` K )
Assertion cdlema1N 
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( X .\/ R ) = ( X .\/ Y ) )

Proof

Step Hyp Ref Expression
1 cdlema1.b 
 |-  B = ( Base ` K )
2 cdlema1.l 
 |-  .<_ = ( le ` K )
3 cdlema1.j 
 |-  .\/ = ( join ` K )
4 cdlema1.m 
 |-  ./\ = ( meet ` K )
5 cdlema1.a 
 |-  A = ( Atoms ` K )
6 cdlema1.n 
 |-  N = ( Lines ` K )
7 cdlema1.f 
 |-  F = ( pmap ` K )
8 simp11 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> K e. HL )
9 8 hllatd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> K e. Lat )
10 simp12 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> X e. B )
11 simp23 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> R e. A )
12 1 5 atbase 
 |-  ( R e. A -> R e. B )
13 11 12 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> R e. B )
14 1 3 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ R e. B ) -> ( X .\/ R ) e. B )
15 9 10 13 14 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( X .\/ R ) e. B )
16 simp13 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> Y e. B )
17 1 3 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
18 9 10 16 17 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( X .\/ Y ) e. B )
19 1 2 3 latlej1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> X .<_ ( X .\/ Y ) )
20 9 10 16 19 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> X .<_ ( X .\/ Y ) )
21 simp21 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> P e. A )
22 1 5 atbase 
 |-  ( P e. A -> P e. B )
23 21 22 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> P e. B )
24 simp22 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> Q e. A )
25 1 5 atbase 
 |-  ( Q e. A -> Q e. B )
26 24 25 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> Q e. B )
27 1 3 latjcl 
 |-  ( ( K e. Lat /\ P e. B /\ Q e. B ) -> ( P .\/ Q ) e. B )
28 9 23 26 27 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( P .\/ Q ) e. B )
29 simp31r 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> R .<_ ( P .\/ Q ) )
30 simp32l 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> P .<_ X )
31 simp32r 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> Q .<_ Y )
32 1 2 3 latjlej12 
 |-  ( ( K e. Lat /\ ( P e. B /\ X e. B ) /\ ( Q e. B /\ Y e. B ) ) -> ( ( P .<_ X /\ Q .<_ Y ) -> ( P .\/ Q ) .<_ ( X .\/ Y ) ) )
33 9 23 10 26 16 32 syl122anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( ( P .<_ X /\ Q .<_ Y ) -> ( P .\/ Q ) .<_ ( X .\/ Y ) ) )
34 30 31 33 mp2and 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( P .\/ Q ) .<_ ( X .\/ Y ) )
35 1 2 9 13 28 18 29 34 lattrd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> R .<_ ( X .\/ Y ) )
36 1 2 3 latjle12 
 |-  ( ( K e. Lat /\ ( X e. B /\ R e. B /\ ( X .\/ Y ) e. B ) ) -> ( ( X .<_ ( X .\/ Y ) /\ R .<_ ( X .\/ Y ) ) <-> ( X .\/ R ) .<_ ( X .\/ Y ) ) )
37 9 10 13 18 36 syl13anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( ( X .<_ ( X .\/ Y ) /\ R .<_ ( X .\/ Y ) ) <-> ( X .\/ R ) .<_ ( X .\/ Y ) ) )
38 20 35 37 mpbi2and 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( X .\/ R ) .<_ ( X .\/ Y ) )
39 1 2 3 latlej1 
 |-  ( ( K e. Lat /\ X e. B /\ R e. B ) -> X .<_ ( X .\/ R ) )
40 9 10 13 39 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> X .<_ ( X .\/ R ) )
41 simp331 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( F ` Y ) e. N )
42 simp332 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( X ./\ Y ) e. A )
43 simp333 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> -. Q .<_ X )
44 1 2 4 latmle1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) .<_ X )
45 9 10 16 44 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( X ./\ Y ) .<_ X )
46 breq1 
 |-  ( Q = ( X ./\ Y ) -> ( Q .<_ X <-> ( X ./\ Y ) .<_ X ) )
47 45 46 syl5ibrcom 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( Q = ( X ./\ Y ) -> Q .<_ X ) )
48 47 necon3bd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( -. Q .<_ X -> Q =/= ( X ./\ Y ) ) )
49 43 48 mpd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> Q =/= ( X ./\ Y ) )
50 1 2 4 latmle2 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) .<_ Y )
51 9 10 16 50 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( X ./\ Y ) .<_ Y )
52 1 2 3 5 6 7 lneq2at 
 |-  ( ( ( K e. HL /\ Y e. B /\ ( F ` Y ) e. N ) /\ ( Q e. A /\ ( X ./\ Y ) e. A /\ Q =/= ( X ./\ Y ) ) /\ ( Q .<_ Y /\ ( X ./\ Y ) .<_ Y ) ) -> Y = ( Q .\/ ( X ./\ Y ) ) )
53 8 16 41 24 42 49 31 51 52 syl332anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> Y = ( Q .\/ ( X ./\ Y ) ) )
54 1 3 latjcl 
 |-  ( ( K e. Lat /\ P e. B /\ R e. B ) -> ( P .\/ R ) e. B )
55 9 23 13 54 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( P .\/ R ) e. B )
56 11 24 21 3jca 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( R e. A /\ Q e. A /\ P e. A ) )
57 simp31l 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> R =/= P )
58 8 56 57 3jca 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( K e. HL /\ ( R e. A /\ Q e. A /\ P e. A ) /\ R =/= P ) )
59 2 3 5 hlatexch1 
 |-  ( ( K e. HL /\ ( R e. A /\ Q e. A /\ P e. A ) /\ R =/= P ) -> ( R .<_ ( P .\/ Q ) -> Q .<_ ( P .\/ R ) ) )
60 58 29 59 sylc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> Q .<_ ( P .\/ R ) )
61 23 10 13 3jca 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( P e. B /\ X e. B /\ R e. B ) )
62 9 61 jca 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( K e. Lat /\ ( P e. B /\ X e. B /\ R e. B ) ) )
63 1 2 3 latjlej1 
 |-  ( ( K e. Lat /\ ( P e. B /\ X e. B /\ R e. B ) ) -> ( P .<_ X -> ( P .\/ R ) .<_ ( X .\/ R ) ) )
64 62 30 63 sylc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( P .\/ R ) .<_ ( X .\/ R ) )
65 1 2 9 26 55 15 60 64 lattrd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> Q .<_ ( X .\/ R ) )
66 1 2 3 4 latmlej11 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ R e. B ) ) -> ( X ./\ Y ) .<_ ( X .\/ R ) )
67 9 10 16 13 66 syl13anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( X ./\ Y ) .<_ ( X .\/ R ) )
68 1 4 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
69 9 10 16 68 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( X ./\ Y ) e. B )
70 1 2 3 latjle12 
 |-  ( ( K e. Lat /\ ( Q e. B /\ ( X ./\ Y ) e. B /\ ( X .\/ R ) e. B ) ) -> ( ( Q .<_ ( X .\/ R ) /\ ( X ./\ Y ) .<_ ( X .\/ R ) ) <-> ( Q .\/ ( X ./\ Y ) ) .<_ ( X .\/ R ) ) )
71 9 26 69 15 70 syl13anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( ( Q .<_ ( X .\/ R ) /\ ( X ./\ Y ) .<_ ( X .\/ R ) ) <-> ( Q .\/ ( X ./\ Y ) ) .<_ ( X .\/ R ) ) )
72 65 67 71 mpbi2and 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( Q .\/ ( X ./\ Y ) ) .<_ ( X .\/ R ) )
73 53 72 eqbrtrd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> Y .<_ ( X .\/ R ) )
74 1 2 3 latjle12 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ ( X .\/ R ) e. B ) ) -> ( ( X .<_ ( X .\/ R ) /\ Y .<_ ( X .\/ R ) ) <-> ( X .\/ Y ) .<_ ( X .\/ R ) ) )
75 9 10 16 15 74 syl13anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( ( X .<_ ( X .\/ R ) /\ Y .<_ ( X .\/ R ) ) <-> ( X .\/ Y ) .<_ ( X .\/ R ) ) )
76 40 73 75 mpbi2and 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( X .\/ Y ) .<_ ( X .\/ R ) )
77 1 2 9 15 18 38 76 latasymd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> ( X .\/ R ) = ( X .\/ Y ) )