Step |
Hyp |
Ref |
Expression |
1 |
|
atexchcvr.j |
|- .\/ = ( join ` K ) |
2 |
|
atexchcvr.a |
|- A = ( Atoms ` K ) |
3 |
|
atexchcvr.c |
|- C = ( |
4 |
|
simpl1 |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ P C ( Q .\/ R ) ) -> K e. HL ) |
5 |
|
simpl21 |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ P C ( Q .\/ R ) ) -> P e. A ) |
6 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
7 |
6 2
|
atbase |
|- ( P e. A -> P e. ( Base ` K ) ) |
8 |
5 7
|
syl |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ P C ( Q .\/ R ) ) -> P e. ( Base ` K ) ) |
9 |
4
|
hllatd |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ P C ( Q .\/ R ) ) -> K e. Lat ) |
10 |
|
simpl22 |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ P C ( Q .\/ R ) ) -> Q e. A ) |
11 |
6 2
|
atbase |
|- ( Q e. A -> Q e. ( Base ` K ) ) |
12 |
10 11
|
syl |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ P C ( Q .\/ R ) ) -> Q e. ( Base ` K ) ) |
13 |
|
simpl23 |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ P C ( Q .\/ R ) ) -> R e. A ) |
14 |
6 2
|
atbase |
|- ( R e. A -> R e. ( Base ` K ) ) |
15 |
13 14
|
syl |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ P C ( Q .\/ R ) ) -> R e. ( Base ` K ) ) |
16 |
6 1
|
latjcl |
|- ( ( K e. Lat /\ Q e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( Q .\/ R ) e. ( Base ` K ) ) |
17 |
9 12 15 16
|
syl3anc |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ P C ( Q .\/ R ) ) -> ( Q .\/ R ) e. ( Base ` K ) ) |
18 |
4 8 17
|
3jca |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ P C ( Q .\/ R ) ) -> ( K e. HL /\ P e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) ) ) |
19 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
20 |
6 19 3
|
cvrle |
|- ( ( ( K e. HL /\ P e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) ) /\ P C ( Q .\/ R ) ) -> P ( le ` K ) ( Q .\/ R ) ) |
21 |
18 20
|
sylancom |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ P C ( Q .\/ R ) ) -> P ( le ` K ) ( Q .\/ R ) ) |
22 |
21
|
ex |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( P C ( Q .\/ R ) -> P ( le ` K ) ( Q .\/ R ) ) ) |
23 |
19 1 2
|
hlatexch2 |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( P ( le ` K ) ( Q .\/ R ) -> Q ( le ` K ) ( P .\/ R ) ) ) |
24 |
|
simpl1 |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ Q ( le ` K ) ( P .\/ R ) ) -> K e. HL ) |
25 |
|
simpl22 |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ Q ( le ` K ) ( P .\/ R ) ) -> Q e. A ) |
26 |
|
simpl21 |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ Q ( le ` K ) ( P .\/ R ) ) -> P e. A ) |
27 |
|
simpl23 |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ Q ( le ` K ) ( P .\/ R ) ) -> R e. A ) |
28 |
|
simpl3 |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ Q ( le ` K ) ( P .\/ R ) ) -> P =/= R ) |
29 |
|
simpr |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ Q ( le ` K ) ( P .\/ R ) ) -> Q ( le ` K ) ( P .\/ R ) ) |
30 |
19 1 3 2
|
atcvrj2 |
|- ( ( K e. HL /\ ( Q e. A /\ P e. A /\ R e. A ) /\ ( P =/= R /\ Q ( le ` K ) ( P .\/ R ) ) ) -> Q C ( P .\/ R ) ) |
31 |
24 25 26 27 28 29 30
|
syl132anc |
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) /\ Q ( le ` K ) ( P .\/ R ) ) -> Q C ( P .\/ R ) ) |
32 |
31
|
ex |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( Q ( le ` K ) ( P .\/ R ) -> Q C ( P .\/ R ) ) ) |
33 |
22 23 32
|
3syld |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( P C ( Q .\/ R ) -> Q C ( P .\/ R ) ) ) |