Step |
Hyp |
Ref |
Expression |
1 |
|
2polss.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
2 |
|
2polss.p |
⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 ) |
3 |
|
hlclat |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat ) |
4 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
5 |
4 1
|
atssbase |
⊢ 𝐴 ⊆ ( Base ‘ 𝐾 ) |
6 |
|
sstr |
⊢ ( ( 𝑆 ⊆ 𝐴 ∧ 𝐴 ⊆ ( Base ‘ 𝐾 ) ) → 𝑆 ⊆ ( Base ‘ 𝐾 ) ) |
7 |
5 6
|
mpan2 |
⊢ ( 𝑆 ⊆ 𝐴 → 𝑆 ⊆ ( Base ‘ 𝐾 ) ) |
8 |
|
eqid |
⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 ) |
9 |
4 8
|
clatlubcl |
⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ ( Base ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
10 |
3 7 9
|
syl2an |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ) → ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
11 |
|
eqid |
⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 ) |
12 |
|
eqid |
⊢ ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 ) |
13 |
4 11 12 2
|
polpmapN |
⊢ ( ( 𝐾 ∈ HL ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ⊥ ‘ ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) ) |
14 |
10 13
|
syldan |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ) → ( ⊥ ‘ ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) ) |
15 |
8 1 12 2
|
2polvalN |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) |
16 |
15
|
fveq2d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) = ( ⊥ ‘ ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) ) |
17 |
8 11 1 12 2
|
polval2N |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑆 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) ) |
18 |
14 16 17
|
3eqtr4d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) = ( ⊥ ‘ 𝑆 ) ) |