Step |
Hyp |
Ref |
Expression |
1 |
|
cdlemeda.l |
|- .<_ = ( le ` K ) |
2 |
|
cdlemeda.j |
|- .\/ = ( join ` K ) |
3 |
|
cdlemeda.m |
|- ./\ = ( meet ` K ) |
4 |
|
cdlemeda.a |
|- A = ( Atoms ` K ) |
5 |
|
cdlemeda.h |
|- H = ( LHyp ` K ) |
6 |
|
cdlemeda.d |
|- D = ( ( R .\/ S ) ./\ W ) |
7 |
|
simp1l |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( R e. A /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> K e. HL ) |
8 |
|
simp31 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( R e. A /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> R e. A ) |
9 |
|
simp2l |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( R e. A /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> S e. A ) |
10 |
2 4
|
hlatjcom |
|- ( ( K e. HL /\ R e. A /\ S e. A ) -> ( R .\/ S ) = ( S .\/ R ) ) |
11 |
7 8 9 10
|
syl3anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( R e. A /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( R .\/ S ) = ( S .\/ R ) ) |
12 |
11
|
oveq1d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( R e. A /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ S ) ./\ W ) = ( ( S .\/ R ) ./\ W ) ) |
13 |
|
simp1r |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( R e. A /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> W e. H ) |
14 |
|
simp2r |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( R e. A /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> -. S .<_ W ) |
15 |
|
simp32 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( R e. A /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> R .<_ ( P .\/ Q ) ) |
16 |
|
simp33 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( R e. A /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> -. S .<_ ( P .\/ Q ) ) |
17 |
1 2 4 5
|
cdlemesner |
|- ( ( K e. HL /\ ( R e. A /\ S e. A ) /\ ( R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> S =/= R ) |
18 |
7 8 9 15 16 17
|
syl122anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( R e. A /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> S =/= R ) |
19 |
1 2 3 4 5
|
lhpat |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( R e. A /\ S =/= R ) ) -> ( ( S .\/ R ) ./\ W ) e. A ) |
20 |
7 13 9 14 8 18 19
|
syl222anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( R e. A /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( S .\/ R ) ./\ W ) e. A ) |
21 |
12 20
|
eqeltrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( R e. A /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ S ) ./\ W ) e. A ) |
22 |
6 21
|
eqeltrid |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( R e. A /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> D e. A ) |