Step |
Hyp |
Ref |
Expression |
1 |
|
cdlemd3.l |
|- .<_ = ( le ` K ) |
2 |
|
cdlemd3.j |
|- .\/ = ( join ` K ) |
3 |
|
cdlemd3.a |
|- A = ( Atoms ` K ) |
4 |
|
cdlemd3.h |
|- H = ( LHyp ` K ) |
5 |
|
simp33 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> -. S .<_ ( P .\/ Q ) ) |
6 |
|
simp1l |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> K e. HL ) |
7 |
|
simp31 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> R e. A ) |
8 |
|
simp32 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> S e. A ) |
9 |
|
simp21l |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> P e. A ) |
10 |
|
simp233 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> R =/= P ) |
11 |
1 2 3
|
hlatexch1 |
|- ( ( K e. HL /\ ( R e. A /\ S e. A /\ P e. A ) /\ R =/= P ) -> ( R .<_ ( P .\/ S ) -> S .<_ ( P .\/ R ) ) ) |
12 |
6 7 8 9 10 11
|
syl131anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> ( R .<_ ( P .\/ S ) -> S .<_ ( P .\/ R ) ) ) |
13 |
|
simp22l |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> Q e. A ) |
14 |
1 2 3
|
hlatlej1 |
|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> P .<_ ( P .\/ Q ) ) |
15 |
6 9 13 14
|
syl3anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> P .<_ ( P .\/ Q ) ) |
16 |
|
simp232 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> R .<_ ( P .\/ Q ) ) |
17 |
6
|
hllatd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> K e. Lat ) |
18 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
19 |
18 3
|
atbase |
|- ( P e. A -> P e. ( Base ` K ) ) |
20 |
9 19
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> P e. ( Base ` K ) ) |
21 |
18 3
|
atbase |
|- ( R e. A -> R e. ( Base ` K ) ) |
22 |
7 21
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> R e. ( Base ` K ) ) |
23 |
18 3
|
atbase |
|- ( Q e. A -> Q e. ( Base ` K ) ) |
24 |
13 23
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> Q e. ( Base ` K ) ) |
25 |
18 2
|
latjcl |
|- ( ( K e. Lat /\ P e. ( Base ` K ) /\ Q e. ( Base ` K ) ) -> ( P .\/ Q ) e. ( Base ` K ) ) |
26 |
17 20 24 25
|
syl3anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) ) |
27 |
18 1 2
|
latjle12 |
|- ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ R e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) ) -> ( ( P .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) <-> ( P .\/ R ) .<_ ( P .\/ Q ) ) ) |
28 |
17 20 22 26 27
|
syl13anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( P .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) <-> ( P .\/ R ) .<_ ( P .\/ Q ) ) ) |
29 |
15 16 28
|
mpbi2and |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> ( P .\/ R ) .<_ ( P .\/ Q ) ) |
30 |
18 3
|
atbase |
|- ( S e. A -> S e. ( Base ` K ) ) |
31 |
8 30
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> S e. ( Base ` K ) ) |
32 |
18 2
|
latjcl |
|- ( ( K e. Lat /\ P e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( P .\/ R ) e. ( Base ` K ) ) |
33 |
17 20 22 32
|
syl3anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> ( P .\/ R ) e. ( Base ` K ) ) |
34 |
18 1
|
lattr |
|- ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ ( P .\/ R ) e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) ) -> ( ( S .<_ ( P .\/ R ) /\ ( P .\/ R ) .<_ ( P .\/ Q ) ) -> S .<_ ( P .\/ Q ) ) ) |
35 |
17 31 33 26 34
|
syl13anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( S .<_ ( P .\/ R ) /\ ( P .\/ R ) .<_ ( P .\/ Q ) ) -> S .<_ ( P .\/ Q ) ) ) |
36 |
29 35
|
mpan2d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> ( S .<_ ( P .\/ R ) -> S .<_ ( P .\/ Q ) ) ) |
37 |
12 36
|
syld |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> ( R .<_ ( P .\/ S ) -> S .<_ ( P .\/ Q ) ) ) |
38 |
5 37
|
mtod |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ S e. A /\ -. S .<_ ( P .\/ Q ) ) ) -> -. R .<_ ( P .\/ S ) ) |