Step |
Hyp |
Ref |
Expression |
1 |
|
2dim.j |
|- .\/ = ( join ` K ) |
2 |
|
2dim.c |
|- C = ( |
3 |
|
2dim.a |
|- A = ( Atoms ` K ) |
4 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
5 |
1 4 3
|
3dim1 |
|- ( ( K e. HL /\ P e. A ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) ) |
6 |
|
df-3an |
|- ( ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) <-> ( ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) ) |
7 |
6
|
rexbii |
|- ( E. s e. A ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) <-> E. s e. A ( ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) ) |
8 |
|
r19.42v |
|- ( E. s e. A ( ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) <-> ( ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) ) /\ E. s e. A -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) ) |
9 |
7 8
|
bitri |
|- ( E. s e. A ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) <-> ( ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) ) /\ E. s e. A -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) ) |
10 |
9
|
simplbi |
|- ( E. s e. A ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) -> ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) ) ) |
11 |
|
simplll |
|- ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> K e. HL ) |
12 |
|
hlatl |
|- ( K e. HL -> K e. AtLat ) |
13 |
11 12
|
syl |
|- ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> K e. AtLat ) |
14 |
|
simplr |
|- ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> q e. A ) |
15 |
|
simpllr |
|- ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> P e. A ) |
16 |
4 3
|
atncmp |
|- ( ( K e. AtLat /\ q e. A /\ P e. A ) -> ( -. q ( le ` K ) P <-> q =/= P ) ) |
17 |
13 14 15 16
|
syl3anc |
|- ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( -. q ( le ` K ) P <-> q =/= P ) ) |
18 |
|
necom |
|- ( q =/= P <-> P =/= q ) |
19 |
17 18
|
bitr2di |
|- ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( P =/= q <-> -. q ( le ` K ) P ) ) |
20 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
21 |
20 3
|
atbase |
|- ( P e. A -> P e. ( Base ` K ) ) |
22 |
15 21
|
syl |
|- ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> P e. ( Base ` K ) ) |
23 |
20 4 1 2 3
|
cvr1 |
|- ( ( K e. HL /\ P e. ( Base ` K ) /\ q e. A ) -> ( -. q ( le ` K ) P <-> P C ( P .\/ q ) ) ) |
24 |
11 22 14 23
|
syl3anc |
|- ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( -. q ( le ` K ) P <-> P C ( P .\/ q ) ) ) |
25 |
19 24
|
bitrd |
|- ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( P =/= q <-> P C ( P .\/ q ) ) ) |
26 |
20 1 3
|
hlatjcl |
|- ( ( K e. HL /\ P e. A /\ q e. A ) -> ( P .\/ q ) e. ( Base ` K ) ) |
27 |
11 15 14 26
|
syl3anc |
|- ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( P .\/ q ) e. ( Base ` K ) ) |
28 |
|
simpr |
|- ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> r e. A ) |
29 |
20 4 1 2 3
|
cvr1 |
|- ( ( K e. HL /\ ( P .\/ q ) e. ( Base ` K ) /\ r e. A ) -> ( -. r ( le ` K ) ( P .\/ q ) <-> ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) ) |
30 |
11 27 28 29
|
syl3anc |
|- ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( -. r ( le ` K ) ( P .\/ q ) <-> ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) ) |
31 |
25 30
|
anbi12d |
|- ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) ) <-> ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) ) ) |
32 |
10 31
|
syl5ib |
|- ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( E. s e. A ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) -> ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) ) ) |
33 |
32
|
reximdva |
|- ( ( ( K e. HL /\ P e. A ) /\ q e. A ) -> ( E. r e. A E. s e. A ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) -> E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) ) ) |
34 |
33
|
reximdva |
|- ( ( K e. HL /\ P e. A ) -> ( E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) -> E. q e. A E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) ) ) |
35 |
5 34
|
mpd |
|- ( ( K e. HL /\ P e. A ) -> E. q e. A E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) ) |