| Step |
Hyp |
Ref |
Expression |
| 1 |
|
polsubsp.a |
|- A = ( Atoms ` K ) |
| 2 |
|
polsubsp.s |
|- S = ( PSubSp ` K ) |
| 3 |
|
polsubsp.p |
|- ._|_ = ( _|_P ` K ) |
| 4 |
|
eqid |
|- ( lub ` K ) = ( lub ` K ) |
| 5 |
|
eqid |
|- ( oc ` K ) = ( oc ` K ) |
| 6 |
|
eqid |
|- ( pmap ` K ) = ( pmap ` K ) |
| 7 |
4 5 1 6 3
|
polval2N |
|- ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) |
| 8 |
|
hllat |
|- ( K e. HL -> K e. Lat ) |
| 9 |
8
|
adantr |
|- ( ( K e. HL /\ X C_ A ) -> K e. Lat ) |
| 10 |
|
hlop |
|- ( K e. HL -> K e. OP ) |
| 11 |
10
|
adantr |
|- ( ( K e. HL /\ X C_ A ) -> K e. OP ) |
| 12 |
|
hlclat |
|- ( K e. HL -> K e. CLat ) |
| 13 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
| 14 |
13 1
|
atssbase |
|- A C_ ( Base ` K ) |
| 15 |
|
sstr |
|- ( ( X C_ A /\ A C_ ( Base ` K ) ) -> X C_ ( Base ` K ) ) |
| 16 |
14 15
|
mpan2 |
|- ( X C_ A -> X C_ ( Base ` K ) ) |
| 17 |
13 4
|
clatlubcl |
|- ( ( K e. CLat /\ X C_ ( Base ` K ) ) -> ( ( lub ` K ) ` X ) e. ( Base ` K ) ) |
| 18 |
12 16 17
|
syl2an |
|- ( ( K e. HL /\ X C_ A ) -> ( ( lub ` K ) ` X ) e. ( Base ` K ) ) |
| 19 |
13 5
|
opoccl |
|- ( ( K e. OP /\ ( ( lub ` K ) ` X ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) ) |
| 20 |
11 18 19
|
syl2anc |
|- ( ( K e. HL /\ X C_ A ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) ) |
| 21 |
13 2 6
|
pmapsub |
|- ( ( K e. Lat /\ ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) ) -> ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) e. S ) |
| 22 |
9 20 21
|
syl2anc |
|- ( ( K e. HL /\ X C_ A ) -> ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) e. S ) |
| 23 |
7 22
|
eqeltrd |
|- ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) e. S ) |