Step |
Hyp |
Ref |
Expression |
1 |
|
cdlemg5.l |
|- .<_ = ( le ` K ) |
2 |
|
cdlemg5.j |
|- .\/ = ( join ` K ) |
3 |
|
cdlemg5.a |
|- A = ( Atoms ` K ) |
4 |
|
cdlemg5.h |
|- H = ( LHyp ` K ) |
5 |
|
simpl1 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q ) -> ( K e. HL /\ W e. H ) ) |
6 |
|
simpl2 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q ) -> ( P e. A /\ -. P .<_ W ) ) |
7 |
1 2 3 4
|
cdlemg5 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> E. r e. A ( P =/= r /\ -. r .<_ W ) ) |
8 |
5 6 7
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q ) -> E. r e. A ( P =/= r /\ -. r .<_ W ) ) |
9 |
|
ancom |
|- ( ( P =/= r /\ -. r .<_ W ) <-> ( -. r .<_ W /\ P =/= r ) ) |
10 |
|
eqcom |
|- ( P = r <-> r = P ) |
11 |
|
simp2 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q /\ r e. A ) -> P = Q ) |
12 |
11
|
oveq2d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q /\ r e. A ) -> ( P .\/ P ) = ( P .\/ Q ) ) |
13 |
|
simp11l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q /\ r e. A ) -> K e. HL ) |
14 |
|
simp12l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q /\ r e. A ) -> P e. A ) |
15 |
2 3
|
hlatjidm |
|- ( ( K e. HL /\ P e. A ) -> ( P .\/ P ) = P ) |
16 |
13 14 15
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q /\ r e. A ) -> ( P .\/ P ) = P ) |
17 |
12 16
|
eqtr3d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q /\ r e. A ) -> ( P .\/ Q ) = P ) |
18 |
17
|
breq2d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q /\ r e. A ) -> ( r .<_ ( P .\/ Q ) <-> r .<_ P ) ) |
19 |
|
hlatl |
|- ( K e. HL -> K e. AtLat ) |
20 |
13 19
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q /\ r e. A ) -> K e. AtLat ) |
21 |
|
simp3 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q /\ r e. A ) -> r e. A ) |
22 |
1 3
|
atcmp |
|- ( ( K e. AtLat /\ r e. A /\ P e. A ) -> ( r .<_ P <-> r = P ) ) |
23 |
20 21 14 22
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q /\ r e. A ) -> ( r .<_ P <-> r = P ) ) |
24 |
18 23
|
bitr2d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q /\ r e. A ) -> ( r = P <-> r .<_ ( P .\/ Q ) ) ) |
25 |
10 24
|
syl5bb |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q /\ r e. A ) -> ( P = r <-> r .<_ ( P .\/ Q ) ) ) |
26 |
25
|
necon3abid |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q /\ r e. A ) -> ( P =/= r <-> -. r .<_ ( P .\/ Q ) ) ) |
27 |
26
|
anbi2d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q /\ r e. A ) -> ( ( -. r .<_ W /\ P =/= r ) <-> ( -. r .<_ W /\ -. r .<_ ( P .\/ Q ) ) ) ) |
28 |
9 27
|
syl5bb |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q /\ r e. A ) -> ( ( P =/= r /\ -. r .<_ W ) <-> ( -. r .<_ W /\ -. r .<_ ( P .\/ Q ) ) ) ) |
29 |
28
|
3expa |
|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q ) /\ r e. A ) -> ( ( P =/= r /\ -. r .<_ W ) <-> ( -. r .<_ W /\ -. r .<_ ( P .\/ Q ) ) ) ) |
30 |
29
|
rexbidva |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q ) -> ( E. r e. A ( P =/= r /\ -. r .<_ W ) <-> E. r e. A ( -. r .<_ W /\ -. r .<_ ( P .\/ Q ) ) ) ) |
31 |
8 30
|
mpbid |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q ) -> E. r e. A ( -. r .<_ W /\ -. r .<_ ( P .\/ Q ) ) ) |
32 |
|
simpl1 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> ( K e. HL /\ W e. H ) ) |
33 |
|
simpl2 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> ( P e. A /\ -. P .<_ W ) ) |
34 |
|
simpl3 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> ( Q e. A /\ -. Q .<_ W ) ) |
35 |
|
simpr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> P =/= Q ) |
36 |
1 2 3 4
|
cdlemb2 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> E. r e. A ( -. r .<_ W /\ -. r .<_ ( P .\/ Q ) ) ) |
37 |
32 33 34 35 36
|
syl121anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> E. r e. A ( -. r .<_ W /\ -. r .<_ ( P .\/ Q ) ) ) |
38 |
31 37
|
pm2.61dane |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> E. r e. A ( -. r .<_ W /\ -. r .<_ ( P .\/ Q ) ) ) |