Step |
Hyp |
Ref |
Expression |
1 |
|
2polss.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
2 |
|
2polss.p |
⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 ) |
3 |
|
simp3 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → 𝑋 ⊆ 𝑌 ) |
4 |
|
iinss1 |
⊢ ( 𝑋 ⊆ 𝑌 → ∩ 𝑝 ∈ 𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ⊆ ∩ 𝑝 ∈ 𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) |
5 |
|
sslin |
⊢ ( ∩ 𝑝 ∈ 𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ⊆ ∩ 𝑝 ∈ 𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) → ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ⊆ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ) |
6 |
3 4 5
|
3syl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ⊆ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ) |
7 |
|
eqid |
⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 ) |
8 |
|
eqid |
⊢ ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 ) |
9 |
7 1 8 2
|
polvalN |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑌 ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ) |
10 |
9
|
3adant3 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑌 ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ) |
11 |
|
simp1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → 𝐾 ∈ HL ) |
12 |
|
simp2 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → 𝑌 ⊆ 𝐴 ) |
13 |
3 12
|
sstrd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → 𝑋 ⊆ 𝐴 ) |
14 |
7 1 8 2
|
polvalN |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑋 ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ) |
15 |
11 13 14
|
syl2anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑋 ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ) |
16 |
6 10 15
|
3sstr4d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) |