Metamath Proof Explorer

Theorem 2llnjaN

Description: The join of two different lattice lines in a lattice plane equals the plane (version of 2llnjN in terms of atoms). (Contributed by NM, 5-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2llnja.l 
|- .<_ = ( le ` K )
2llnja.j 
|- .\/ = ( join ` K )
2llnja.a 
|- A = ( Atoms ` K )
2llnja.n 
|- N = ( LLines ` K )
2llnja.p 
|- P = ( LPlanes ` K )
Assertion 2llnjaN 
|- ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( ( Q .\/ R ) .\/ ( S .\/ T ) ) = W )

Proof

Step Hyp Ref Expression
1 2llnja.l 
 |-  .<_ = ( le ` K )
2 2llnja.j 
 |-  .\/ = ( join ` K )
3 2llnja.a 
 |-  A = ( Atoms ` K )
4 2llnja.n 
 |-  N = ( LLines ` K )
5 2llnja.p 
 |-  P = ( LPlanes ` K )
6 eqid 
 |-  ( Base ` K ) = ( Base ` K )
7 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> K e. HL )
8 7 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> K e. Lat )
9 simpl21 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> Q e. A )
10 simpl22 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> R e. A )
11 6 2 3 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) e. ( Base ` K ) )
12 7 9 10 11 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( Q .\/ R ) e. ( Base ` K ) )
13 simpl31 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> S e. A )
14 simpl32 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> T e. A )
15 6 2 3 hlatjcl 
 |-  ( ( K e. HL /\ S e. A /\ T e. A ) -> ( S .\/ T ) e. ( Base ` K ) )
16 7 13 14 15 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( S .\/ T ) e. ( Base ` K ) )
17 6 2 latjcl 
 |-  ( ( K e. Lat /\ ( Q .\/ R ) e. ( Base ` K ) /\ ( S .\/ T ) e. ( Base ` K ) ) -> ( ( Q .\/ R ) .\/ ( S .\/ T ) ) e. ( Base ` K ) )
18 8 12 16 17 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( ( Q .\/ R ) .\/ ( S .\/ T ) ) e. ( Base ` K ) )
19 simpl1r 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> W e. P )
20 6 5 lplnbase 
 |-  ( W e. P -> W e. ( Base ` K ) )
21 19 20 syl 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> W e. ( Base ` K ) )
22 simpr1 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( Q .\/ R ) .<_ W )
23 simpr2 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( S .\/ T ) .<_ W )
24 6 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( ( Q .\/ R ) e. ( Base ` K ) /\ ( S .\/ T ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W ) <-> ( ( Q .\/ R ) .\/ ( S .\/ T ) ) .<_ W ) )
25 8 12 16 21 24 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W ) <-> ( ( Q .\/ R ) .\/ ( S .\/ T ) ) .<_ W ) )
26 22 23 25 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( ( Q .\/ R ) .\/ ( S .\/ T ) ) .<_ W )
27 6 3 atbase 
 |-  ( T e. A -> T e. ( Base ` K ) )
28 14 27 syl 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> T e. ( Base ` K ) )
29 6 2 latjcl 
 |-  ( ( K e. Lat /\ ( Q .\/ R ) e. ( Base ` K ) /\ T e. ( Base ` K ) ) -> ( ( Q .\/ R ) .\/ T ) e. ( Base ` K ) )
30 8 12 28 29 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( ( Q .\/ R ) .\/ T ) e. ( Base ` K ) )
31 6 3 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
32 13 31 syl 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> S e. ( Base ` K ) )
33 6 1 2 latlej2 
 |-  ( ( K e. Lat /\ S e. ( Base ` K ) /\ T e. ( Base ` K ) ) -> T .<_ ( S .\/ T ) )
34 8 32 28 33 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> T .<_ ( S .\/ T ) )
35 6 1 2 latjlej2 
 |-  ( ( K e. Lat /\ ( T e. ( Base ` K ) /\ ( S .\/ T ) e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) ) ) -> ( T .<_ ( S .\/ T ) -> ( ( Q .\/ R ) .\/ T ) .<_ ( ( Q .\/ R ) .\/ ( S .\/ T ) ) ) )
36 8 28 16 12 35 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( T .<_ ( S .\/ T ) -> ( ( Q .\/ R ) .\/ T ) .<_ ( ( Q .\/ R ) .\/ ( S .\/ T ) ) ) )
37 34 36 mpd 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( ( Q .\/ R ) .\/ T ) .<_ ( ( Q .\/ R ) .\/ ( S .\/ T ) ) )
38 6 1 8 30 18 21 37 26 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( ( Q .\/ R ) .\/ T ) .<_ W )
39 38 3adant3 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> ( ( Q .\/ R ) .\/ T ) .<_ W )
40 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> K e. HL )
41 simp121 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> Q e. A )
42 simp122 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> R e. A )
43 simp132 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> T e. A )
44 simp123 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> Q =/= R )
45 simp23 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> ( Q .\/ R ) =/= ( S .\/ T ) )
46 simpl3 
 |-  ( ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) /\ T .<_ ( Q .\/ R ) ) -> S .<_ ( Q .\/ R ) )
47 simpr 
 |-  ( ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) /\ T .<_ ( Q .\/ R ) ) -> T .<_ ( Q .\/ R ) )
48 6 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ T e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) ) ) -> ( ( S .<_ ( Q .\/ R ) /\ T .<_ ( Q .\/ R ) ) <-> ( S .\/ T ) .<_ ( Q .\/ R ) ) )
49 8 32 28 12 48 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( ( S .<_ ( Q .\/ R ) /\ T .<_ ( Q .\/ R ) ) <-> ( S .\/ T ) .<_ ( Q .\/ R ) ) )
50 49 3adant3 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> ( ( S .<_ ( Q .\/ R ) /\ T .<_ ( Q .\/ R ) ) <-> ( S .\/ T ) .<_ ( Q .\/ R ) ) )
51 50 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) /\ T .<_ ( Q .\/ R ) ) -> ( ( S .<_ ( Q .\/ R ) /\ T .<_ ( Q .\/ R ) ) <-> ( S .\/ T ) .<_ ( Q .\/ R ) ) )
52 46 47 51 mpbi2and 
 |-  ( ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) /\ T .<_ ( Q .\/ R ) ) -> ( S .\/ T ) .<_ ( Q .\/ R ) )
53 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( S e. A /\ T e. A /\ S =/= T ) )
54 1 2 3 ps-1 
 |-  ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) /\ ( Q e. A /\ R e. A ) ) -> ( ( S .\/ T ) .<_ ( Q .\/ R ) <-> ( S .\/ T ) = ( Q .\/ R ) ) )
55 7 53 9 10 54 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( ( S .\/ T ) .<_ ( Q .\/ R ) <-> ( S .\/ T ) = ( Q .\/ R ) ) )
56 55 3adant3 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> ( ( S .\/ T ) .<_ ( Q .\/ R ) <-> ( S .\/ T ) = ( Q .\/ R ) ) )
57 56 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) /\ T .<_ ( Q .\/ R ) ) -> ( ( S .\/ T ) .<_ ( Q .\/ R ) <-> ( S .\/ T ) = ( Q .\/ R ) ) )
58 52 57 mpbid 
 |-  ( ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) /\ T .<_ ( Q .\/ R ) ) -> ( S .\/ T ) = ( Q .\/ R ) )
59 58 eqcomd 
 |-  ( ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) /\ T .<_ ( Q .\/ R ) ) -> ( Q .\/ R ) = ( S .\/ T ) )
60 59 ex 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> ( T .<_ ( Q .\/ R ) -> ( Q .\/ R ) = ( S .\/ T ) ) )
61 60 necon3ad 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> ( ( Q .\/ R ) =/= ( S .\/ T ) -> -. T .<_ ( Q .\/ R ) ) )
62 45 61 mpd 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> -. T .<_ ( Q .\/ R ) )
63 1 2 3 5 lplni2 
 |-  ( ( K e. HL /\ ( Q e. A /\ R e. A /\ T e. A ) /\ ( Q =/= R /\ -. T .<_ ( Q .\/ R ) ) ) -> ( ( Q .\/ R ) .\/ T ) e. P )
64 40 41 42 43 44 62 63 syl132anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> ( ( Q .\/ R ) .\/ T ) e. P )
65 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> W e. P )
66 1 5 lplncmp 
 |-  ( ( K e. HL /\ ( ( Q .\/ R ) .\/ T ) e. P /\ W e. P ) -> ( ( ( Q .\/ R ) .\/ T ) .<_ W <-> ( ( Q .\/ R ) .\/ T ) = W ) )
67 40 64 65 66 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> ( ( ( Q .\/ R ) .\/ T ) .<_ W <-> ( ( Q .\/ R ) .\/ T ) = W ) )
68 39 67 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> ( ( Q .\/ R ) .\/ T ) = W )
69 37 3adant3 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> ( ( Q .\/ R ) .\/ T ) .<_ ( ( Q .\/ R ) .\/ ( S .\/ T ) ) )
70 68 69 eqbrtrrd 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ S .<_ ( Q .\/ R ) ) -> W .<_ ( ( Q .\/ R ) .\/ ( S .\/ T ) ) )
71 70 3expia 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( S .<_ ( Q .\/ R ) -> W .<_ ( ( Q .\/ R ) .\/ ( S .\/ T ) ) ) )
72 6 2 latjcl 
 |-  ( ( K e. Lat /\ ( Q .\/ R ) e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> ( ( Q .\/ R ) .\/ S ) e. ( Base ` K ) )
73 8 12 32 72 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( ( Q .\/ R ) .\/ S ) e. ( Base ` K ) )
74 6 1 2 latlej1 
 |-  ( ( K e. Lat /\ S e. ( Base ` K ) /\ T e. ( Base ` K ) ) -> S .<_ ( S .\/ T ) )
75 8 32 28 74 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> S .<_ ( S .\/ T ) )
76 6 1 2 latjlej2 
 |-  ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ ( S .\/ T ) e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) ) ) -> ( S .<_ ( S .\/ T ) -> ( ( Q .\/ R ) .\/ S ) .<_ ( ( Q .\/ R ) .\/ ( S .\/ T ) ) ) )
77 8 32 16 12 76 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( S .<_ ( S .\/ T ) -> ( ( Q .\/ R ) .\/ S ) .<_ ( ( Q .\/ R ) .\/ ( S .\/ T ) ) ) )
78 75 77 mpd 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( ( Q .\/ R ) .\/ S ) .<_ ( ( Q .\/ R ) .\/ ( S .\/ T ) ) )
79 6 1 8 73 18 21 78 26 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( ( Q .\/ R ) .\/ S ) .<_ W )
80 79 3adant3 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ -. S .<_ ( Q .\/ R ) ) -> ( ( Q .\/ R ) .\/ S ) .<_ W )
81 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ -. S .<_ ( Q .\/ R ) ) -> K e. HL )
82 simp121 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ -. S .<_ ( Q .\/ R ) ) -> Q e. A )
83 simp122 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ -. S .<_ ( Q .\/ R ) ) -> R e. A )
84 simp131 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ -. S .<_ ( Q .\/ R ) ) -> S e. A )
85 simp123 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ -. S .<_ ( Q .\/ R ) ) -> Q =/= R )
86 simp3 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ -. S .<_ ( Q .\/ R ) ) -> -. S .<_ ( Q .\/ R ) )
87 1 2 3 5 lplni2 
 |-  ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ ( Q =/= R /\ -. S .<_ ( Q .\/ R ) ) ) -> ( ( Q .\/ R ) .\/ S ) e. P )
88 81 82 83 84 85 86 87 syl132anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ -. S .<_ ( Q .\/ R ) ) -> ( ( Q .\/ R ) .\/ S ) e. P )
89 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ -. S .<_ ( Q .\/ R ) ) -> W e. P )
90 1 5 lplncmp 
 |-  ( ( K e. HL /\ ( ( Q .\/ R ) .\/ S ) e. P /\ W e. P ) -> ( ( ( Q .\/ R ) .\/ S ) .<_ W <-> ( ( Q .\/ R ) .\/ S ) = W ) )
91 81 88 89 90 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ -. S .<_ ( Q .\/ R ) ) -> ( ( ( Q .\/ R ) .\/ S ) .<_ W <-> ( ( Q .\/ R ) .\/ S ) = W ) )
92 80 91 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ -. S .<_ ( Q .\/ R ) ) -> ( ( Q .\/ R ) .\/ S ) = W )
93 78 3adant3 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ -. S .<_ ( Q .\/ R ) ) -> ( ( Q .\/ R ) .\/ S ) .<_ ( ( Q .\/ R ) .\/ ( S .\/ T ) ) )
94 92 93 eqbrtrrd 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) /\ -. S .<_ ( Q .\/ R ) ) -> W .<_ ( ( Q .\/ R ) .\/ ( S .\/ T ) ) )
95 94 3expia 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( -. S .<_ ( Q .\/ R ) -> W .<_ ( ( Q .\/ R ) .\/ ( S .\/ T ) ) ) )
96 71 95 pm2.61d 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> W .<_ ( ( Q .\/ R ) .\/ ( S .\/ T ) ) )
97 6 1 8 18 21 26 96 latasymd 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( ( Q .\/ R ) .<_ W /\ ( S .\/ T ) .<_ W /\ ( Q .\/ R ) =/= ( S .\/ T ) ) ) -> ( ( Q .\/ R ) .\/ ( S .\/ T ) ) = W )