Step |
Hyp |
Ref |
Expression |
1 |
|
2polat.a |
|- A = ( Atoms ` K ) |
2 |
|
2polat.p |
|- P = ( _|_P ` K ) |
3 |
1 2
|
2polssN |
|- ( ( K e. HL /\ X C_ A ) -> X C_ ( P ` ( P ` X ) ) ) |
4 |
3
|
ssrind |
|- ( ( K e. HL /\ X C_ A ) -> ( X i^i ( P ` X ) ) C_ ( ( P ` ( P ` X ) ) i^i ( P ` X ) ) ) |
5 |
|
eqid |
|- ( lub ` K ) = ( lub ` K ) |
6 |
|
eqid |
|- ( pmap ` K ) = ( pmap ` K ) |
7 |
5 1 6 2
|
2polvalN |
|- ( ( K e. HL /\ X C_ A ) -> ( P ` ( P ` X ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) ) |
8 |
|
eqid |
|- ( oc ` K ) = ( oc ` K ) |
9 |
5 8 1 6 2
|
polval2N |
|- ( ( K e. HL /\ X C_ A ) -> ( P ` X ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) |
10 |
7 9
|
ineq12d |
|- ( ( K e. HL /\ X C_ A ) -> ( ( P ` ( P ` X ) ) i^i ( P ` X ) ) = ( ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) i^i ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) ) |
11 |
|
hlop |
|- ( K e. HL -> K e. OP ) |
12 |
11
|
adantr |
|- ( ( K e. HL /\ X C_ A ) -> K e. OP ) |
13 |
|
hlclat |
|- ( K e. HL -> K e. CLat ) |
14 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
15 |
14 1
|
atssbase |
|- A C_ ( Base ` K ) |
16 |
|
sstr |
|- ( ( X C_ A /\ A C_ ( Base ` K ) ) -> X C_ ( Base ` K ) ) |
17 |
15 16
|
mpan2 |
|- ( X C_ A -> X C_ ( Base ` K ) ) |
18 |
14 5
|
clatlubcl |
|- ( ( K e. CLat /\ X C_ ( Base ` K ) ) -> ( ( lub ` K ) ` X ) e. ( Base ` K ) ) |
19 |
13 17 18
|
syl2an |
|- ( ( K e. HL /\ X C_ A ) -> ( ( lub ` K ) ` X ) e. ( Base ` K ) ) |
20 |
|
eqid |
|- ( meet ` K ) = ( meet ` K ) |
21 |
|
eqid |
|- ( 0. ` K ) = ( 0. ` K ) |
22 |
14 8 20 21
|
opnoncon |
|- ( ( K e. OP /\ ( ( lub ` K ) ` X ) e. ( Base ` K ) ) -> ( ( ( lub ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) = ( 0. ` K ) ) |
23 |
12 19 22
|
syl2anc |
|- ( ( K e. HL /\ X C_ A ) -> ( ( ( lub ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) = ( 0. ` K ) ) |
24 |
23
|
fveq2d |
|- ( ( K e. HL /\ X C_ A ) -> ( ( pmap ` K ) ` ( ( ( lub ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) = ( ( pmap ` K ) ` ( 0. ` K ) ) ) |
25 |
|
simpl |
|- ( ( K e. HL /\ X C_ A ) -> K e. HL ) |
26 |
14 8
|
opoccl |
|- ( ( K e. OP /\ ( ( lub ` K ) ` X ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) ) |
27 |
12 19 26
|
syl2anc |
|- ( ( K e. HL /\ X C_ A ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) ) |
28 |
14 20 1 6
|
pmapmeet |
|- ( ( K e. HL /\ ( ( lub ` K ) ` X ) e. ( Base ` K ) /\ ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) ) -> ( ( pmap ` K ) ` ( ( ( lub ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) = ( ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) i^i ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) ) |
29 |
25 19 27 28
|
syl3anc |
|- ( ( K e. HL /\ X C_ A ) -> ( ( pmap ` K ) ` ( ( ( lub ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) = ( ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) i^i ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) ) |
30 |
|
hlatl |
|- ( K e. HL -> K e. AtLat ) |
31 |
30
|
adantr |
|- ( ( K e. HL /\ X C_ A ) -> K e. AtLat ) |
32 |
21 6
|
pmap0 |
|- ( K e. AtLat -> ( ( pmap ` K ) ` ( 0. ` K ) ) = (/) ) |
33 |
31 32
|
syl |
|- ( ( K e. HL /\ X C_ A ) -> ( ( pmap ` K ) ` ( 0. ` K ) ) = (/) ) |
34 |
24 29 33
|
3eqtr3d |
|- ( ( K e. HL /\ X C_ A ) -> ( ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) i^i ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) = (/) ) |
35 |
10 34
|
eqtrd |
|- ( ( K e. HL /\ X C_ A ) -> ( ( P ` ( P ` X ) ) i^i ( P ` X ) ) = (/) ) |
36 |
4 35
|
sseqtrd |
|- ( ( K e. HL /\ X C_ A ) -> ( X i^i ( P ` X ) ) C_ (/) ) |
37 |
|
ss0b |
|- ( ( X i^i ( P ` X ) ) C_ (/) <-> ( X i^i ( P ` X ) ) = (/) ) |
38 |
36 37
|
sylib |
|- ( ( K e. HL /\ X C_ A ) -> ( X i^i ( P ` X ) ) = (/) ) |