| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cvlatexch.l |
|- .<_ = ( le ` K ) |
| 2 |
|
cvlatexch.j |
|- .\/ = ( join ` K ) |
| 3 |
|
cvlatexch.a |
|- A = ( Atoms ` K ) |
| 4 |
1 2 3
|
cvlatexchb1 |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( P .<_ ( R .\/ Q ) <-> ( R .\/ P ) = ( R .\/ Q ) ) ) |
| 5 |
|
cvllat |
|- ( K e. CvLat -> K e. Lat ) |
| 6 |
5
|
3ad2ant1 |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> K e. Lat ) |
| 7 |
|
simp23 |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> R e. A ) |
| 8 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
| 9 |
8 3
|
atbase |
|- ( R e. A -> R e. ( Base ` K ) ) |
| 10 |
7 9
|
syl |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> R e. ( Base ` K ) ) |
| 11 |
|
simp22 |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> Q e. A ) |
| 12 |
8 3
|
atbase |
|- ( Q e. A -> Q e. ( Base ` K ) ) |
| 13 |
11 12
|
syl |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> Q e. ( Base ` K ) ) |
| 14 |
8 1 2
|
latlej2 |
|- ( ( K e. Lat /\ R e. ( Base ` K ) /\ Q e. ( Base ` K ) ) -> Q .<_ ( R .\/ Q ) ) |
| 15 |
6 10 13 14
|
syl3anc |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> Q .<_ ( R .\/ Q ) ) |
| 16 |
|
breq2 |
|- ( ( R .\/ P ) = ( R .\/ Q ) -> ( Q .<_ ( R .\/ P ) <-> Q .<_ ( R .\/ Q ) ) ) |
| 17 |
15 16
|
syl5ibrcom |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( ( R .\/ P ) = ( R .\/ Q ) -> Q .<_ ( R .\/ P ) ) ) |
| 18 |
4 17
|
sylbid |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( P .<_ ( R .\/ Q ) -> Q .<_ ( R .\/ P ) ) ) |