Step |
Hyp |
Ref |
Expression |
1 |
|
cdlemf1.l |
|- .<_ = ( le ` K ) |
2 |
|
cdlemf1.j |
|- .\/ = ( join ` K ) |
3 |
|
cdlemf1.a |
|- A = ( Atoms ` K ) |
4 |
|
cdlemf1.h |
|- H = ( LHyp ` K ) |
5 |
|
cdlemf2.m |
|- ./\ = ( meet ` K ) |
6 |
1 3 4
|
lhpexnle |
|- ( ( K e. HL /\ W e. H ) -> E. p e. A -. p .<_ W ) |
7 |
6
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> E. p e. A -. p .<_ W ) |
8 |
1 2 3 4
|
cdlemf1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) -> E. q e. A ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) |
9 |
|
simpr1r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> -. p .<_ W ) |
10 |
|
simpr32 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> -. q .<_ W ) |
11 |
|
simpr33 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> U .<_ ( p .\/ q ) ) |
12 |
|
simplrr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> U .<_ W ) |
13 |
|
hllat |
|- ( K e. HL -> K e. Lat ) |
14 |
13
|
ad3antrrr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> K e. Lat ) |
15 |
|
simplrl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> U e. A ) |
16 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
17 |
16 3
|
atbase |
|- ( U e. A -> U e. ( Base ` K ) ) |
18 |
15 17
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> U e. ( Base ` K ) ) |
19 |
|
simplll |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> K e. HL ) |
20 |
|
simpr1l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> p e. A ) |
21 |
|
simpr2 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> q e. A ) |
22 |
16 2 3
|
hlatjcl |
|- ( ( K e. HL /\ p e. A /\ q e. A ) -> ( p .\/ q ) e. ( Base ` K ) ) |
23 |
19 20 21 22
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> ( p .\/ q ) e. ( Base ` K ) ) |
24 |
16 4
|
lhpbase |
|- ( W e. H -> W e. ( Base ` K ) ) |
25 |
24
|
ad3antlr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> W e. ( Base ` K ) ) |
26 |
16 1 5
|
latlem12 |
|- ( ( K e. Lat /\ ( U e. ( Base ` K ) /\ ( p .\/ q ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( U .<_ ( p .\/ q ) /\ U .<_ W ) <-> U .<_ ( ( p .\/ q ) ./\ W ) ) ) |
27 |
14 18 23 25 26
|
syl13anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> ( ( U .<_ ( p .\/ q ) /\ U .<_ W ) <-> U .<_ ( ( p .\/ q ) ./\ W ) ) ) |
28 |
11 12 27
|
mpbi2and |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> U .<_ ( ( p .\/ q ) ./\ W ) ) |
29 |
|
hlatl |
|- ( K e. HL -> K e. AtLat ) |
30 |
29
|
ad3antrrr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> K e. AtLat ) |
31 |
|
simpll |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> ( K e. HL /\ W e. H ) ) |
32 |
|
simpr31 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> p =/= q ) |
33 |
1 2 5 3 4
|
lhpat |
|- ( ( ( K e. HL /\ W e. H ) /\ ( p e. A /\ -. p .<_ W ) /\ ( q e. A /\ p =/= q ) ) -> ( ( p .\/ q ) ./\ W ) e. A ) |
34 |
31 20 9 21 32 33
|
syl122anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> ( ( p .\/ q ) ./\ W ) e. A ) |
35 |
1 3
|
atcmp |
|- ( ( K e. AtLat /\ U e. A /\ ( ( p .\/ q ) ./\ W ) e. A ) -> ( U .<_ ( ( p .\/ q ) ./\ W ) <-> U = ( ( p .\/ q ) ./\ W ) ) ) |
36 |
30 15 34 35
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> ( U .<_ ( ( p .\/ q ) ./\ W ) <-> U = ( ( p .\/ q ) ./\ W ) ) ) |
37 |
28 36
|
mpbid |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> U = ( ( p .\/ q ) ./\ W ) ) |
38 |
9 10 37
|
jca31 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( ( p e. A /\ -. p .<_ W ) /\ q e. A /\ ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) ) ) -> ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p .\/ q ) ./\ W ) ) ) |
39 |
38
|
3exp2 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> ( ( p e. A /\ -. p .<_ W ) -> ( q e. A -> ( ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) -> ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p .\/ q ) ./\ W ) ) ) ) ) ) |
40 |
39
|
3impia |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) -> ( q e. A -> ( ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) -> ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p .\/ q ) ./\ W ) ) ) ) ) |
41 |
40
|
reximdvai |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) -> ( E. q e. A ( p =/= q /\ -. q .<_ W /\ U .<_ ( p .\/ q ) ) -> E. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p .\/ q ) ./\ W ) ) ) ) |
42 |
8 41
|
mpd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ -. p .<_ W ) ) -> E. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p .\/ q ) ./\ W ) ) ) |
43 |
42
|
3expia |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> ( ( p e. A /\ -. p .<_ W ) -> E. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p .\/ q ) ./\ W ) ) ) ) |
44 |
43
|
expd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> ( p e. A -> ( -. p .<_ W -> E. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p .\/ q ) ./\ W ) ) ) ) ) |
45 |
44
|
reximdvai |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> ( E. p e. A -. p .<_ W -> E. p e. A E. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p .\/ q ) ./\ W ) ) ) ) |
46 |
7 45
|
mpd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> E. p e. A E. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p .\/ q ) ./\ W ) ) ) |