Step |
Hyp |
Ref |
Expression |
1 |
|
3noncol.l |
|- .<_ = ( le ` K ) |
2 |
|
3noncol.j |
|- .\/ = ( join ` K ) |
3 |
|
3noncol.a |
|- A = ( Atoms ` K ) |
4 |
|
simp11 |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> K e. HL ) |
5 |
4
|
hllatd |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> K e. Lat ) |
6 |
|
simp2l |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> R e. A ) |
7 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
8 |
7 3
|
atbase |
|- ( R e. A -> R e. ( Base ` K ) ) |
9 |
6 8
|
syl |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> R e. ( Base ` K ) ) |
10 |
|
simp12 |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> P e. A ) |
11 |
7 3
|
atbase |
|- ( P e. A -> P e. ( Base ` K ) ) |
12 |
10 11
|
syl |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> P e. ( Base ` K ) ) |
13 |
|
simp13 |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> Q e. A ) |
14 |
7 3
|
atbase |
|- ( Q e. A -> Q e. ( Base ` K ) ) |
15 |
13 14
|
syl |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> Q e. ( Base ` K ) ) |
16 |
|
simp32 |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> -. R .<_ ( P .\/ Q ) ) |
17 |
7 1 2
|
latnlej1r |
|- ( ( K e. Lat /\ ( R e. ( Base ` K ) /\ P e. ( Base ` K ) /\ Q e. ( Base ` K ) ) /\ -. R .<_ ( P .\/ Q ) ) -> R =/= Q ) |
18 |
5 9 12 15 16 17
|
syl131anc |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> R =/= Q ) |
19 |
18
|
necomd |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> Q =/= R ) |
20 |
|
simp2r |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> S e. A ) |
21 |
7 3
|
atbase |
|- ( S e. A -> S e. ( Base ` K ) ) |
22 |
20 21
|
syl |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> S e. ( Base ` K ) ) |
23 |
7 2
|
latjcl |
|- ( ( K e. Lat /\ Q e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( Q .\/ R ) e. ( Base ` K ) ) |
24 |
5 15 9 23
|
syl3anc |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( Q .\/ R ) e. ( Base ` K ) ) |
25 |
|
simp33 |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> -. S .<_ ( ( P .\/ Q ) .\/ R ) ) |
26 |
2 3
|
hlatjass |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( P .\/ Q ) .\/ R ) = ( P .\/ ( Q .\/ R ) ) ) |
27 |
4 10 13 6 26
|
syl13anc |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( P .\/ Q ) .\/ R ) = ( P .\/ ( Q .\/ R ) ) ) |
28 |
27
|
breq2d |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( S .<_ ( ( P .\/ Q ) .\/ R ) <-> S .<_ ( P .\/ ( Q .\/ R ) ) ) ) |
29 |
25 28
|
mtbid |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> -. S .<_ ( P .\/ ( Q .\/ R ) ) ) |
30 |
7 1 2
|
latnlej2r |
|- ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ P e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) ) /\ -. S .<_ ( P .\/ ( Q .\/ R ) ) ) -> -. S .<_ ( Q .\/ R ) ) |
31 |
5 22 12 24 29 30
|
syl131anc |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> -. S .<_ ( Q .\/ R ) ) |
32 |
|
simp31 |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> P =/= Q ) |
33 |
1 2 3
|
hlatexch1 |
|- ( ( K e. HL /\ ( P e. A /\ R e. A /\ Q e. A ) /\ P =/= Q ) -> ( P .<_ ( Q .\/ R ) -> R .<_ ( Q .\/ P ) ) ) |
34 |
4 10 6 13 32 33
|
syl131anc |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( P .<_ ( Q .\/ R ) -> R .<_ ( Q .\/ P ) ) ) |
35 |
7 2
|
latjcom |
|- ( ( K e. Lat /\ P e. ( Base ` K ) /\ Q e. ( Base ` K ) ) -> ( P .\/ Q ) = ( Q .\/ P ) ) |
36 |
5 12 15 35
|
syl3anc |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( P .\/ Q ) = ( Q .\/ P ) ) |
37 |
36
|
breq2d |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( R .<_ ( P .\/ Q ) <-> R .<_ ( Q .\/ P ) ) ) |
38 |
34 37
|
sylibrd |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( P .<_ ( Q .\/ R ) -> R .<_ ( P .\/ Q ) ) ) |
39 |
16 38
|
mtod |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> -. P .<_ ( Q .\/ R ) ) |
40 |
7 1 2 3
|
hlexch1 |
|- ( ( K e. HL /\ ( P e. A /\ S e. A /\ ( Q .\/ R ) e. ( Base ` K ) ) /\ -. P .<_ ( Q .\/ R ) ) -> ( P .<_ ( ( Q .\/ R ) .\/ S ) -> S .<_ ( ( Q .\/ R ) .\/ P ) ) ) |
41 |
4 10 20 24 39 40
|
syl131anc |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( P .<_ ( ( Q .\/ R ) .\/ S ) -> S .<_ ( ( Q .\/ R ) .\/ P ) ) ) |
42 |
7 2
|
latjcom |
|- ( ( K e. Lat /\ Q e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( Q .\/ R ) = ( R .\/ Q ) ) |
43 |
5 15 9 42
|
syl3anc |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( Q .\/ R ) = ( R .\/ Q ) ) |
44 |
43
|
oveq1d |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( Q .\/ R ) .\/ P ) = ( ( R .\/ Q ) .\/ P ) ) |
45 |
7 2
|
latj31 |
|- ( ( K e. Lat /\ ( R e. ( Base ` K ) /\ Q e. ( Base ` K ) /\ P e. ( Base ` K ) ) ) -> ( ( R .\/ Q ) .\/ P ) = ( ( P .\/ Q ) .\/ R ) ) |
46 |
5 9 15 12 45
|
syl13anc |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( R .\/ Q ) .\/ P ) = ( ( P .\/ Q ) .\/ R ) ) |
47 |
44 46
|
eqtrd |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( Q .\/ R ) .\/ P ) = ( ( P .\/ Q ) .\/ R ) ) |
48 |
47
|
breq2d |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( S .<_ ( ( Q .\/ R ) .\/ P ) <-> S .<_ ( ( P .\/ Q ) .\/ R ) ) ) |
49 |
41 48
|
sylibd |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( P .<_ ( ( Q .\/ R ) .\/ S ) -> S .<_ ( ( P .\/ Q ) .\/ R ) ) ) |
50 |
25 49
|
mtod |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> -. P .<_ ( ( Q .\/ R ) .\/ S ) ) |
51 |
19 31 50
|
3jca |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( Q =/= R /\ -. S .<_ ( Q .\/ R ) /\ -. P .<_ ( ( Q .\/ R ) .\/ S ) ) ) |