Metamath Proof Explorer

Theorem 2polvalN

Description: Value of double polarity. (Contributed by NM, 25-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2polval.u ⊢U=lub⁡K
2polval.a ⊢A=Atoms⁡K
2polval.m ⊢M=pmap⁡K
2polval.p ⊢⊥˙=⊥𝑃⁡K
Assertion 2polvalN ⊢K∈HL∧X⊆A→⊥˙⁡⊥˙⁡X=M⁡U⁡X

Proof

Step Hyp Ref Expression
1 2polval.u ⊢U=lub⁡K
2 2polval.a ⊢A=Atoms⁡K
3 2polval.m ⊢M=pmap⁡K
4 2polval.p ⊢⊥˙=⊥𝑃⁡K
5 eqid ⊢oc⁡K=oc⁡K
6 1 5 2 3 4 polval2N ⊢K∈HL∧X⊆A→⊥˙⁡X=M⁡oc⁡K⁡U⁡X
7 6 fveq2d ⊢K∈HL∧X⊆A→⊥˙⁡⊥˙⁡X=⊥˙⁡M⁡oc⁡K⁡U⁡X
8 hlop ⊢K∈HL→K∈OP
9 8 adantr ⊢K∈HL∧X⊆A→K∈OP
10 hlclat ⊢K∈HL→K∈CLat
11 eqid ⊢BaseK=BaseK
12 11 2 atssbase ⊢A⊆BaseK
13 sstr ⊢X⊆A∧A⊆BaseK→X⊆BaseK
14 12 13 mpan2 ⊢X⊆A→X⊆BaseK
15 11 1 clatlubcl ⊢K∈CLat∧X⊆BaseK→U⁡X∈BaseK
16 10 14 15 syl2an ⊢K∈HL∧X⊆A→U⁡X∈BaseK
17 11 5 opoccl ⊢K∈OP∧U⁡X∈BaseK→oc⁡K⁡U⁡X∈BaseK
18 9 16 17 syl2anc ⊢K∈HL∧X⊆A→oc⁡K⁡U⁡X∈BaseK
19 11 5 3 4 polpmapN ⊢K∈HL∧oc⁡K⁡U⁡X∈BaseK→⊥˙⁡M⁡oc⁡K⁡U⁡X=M⁡oc⁡K⁡oc⁡K⁡U⁡X
20 18 19 syldan ⊢K∈HL∧X⊆A→⊥˙⁡M⁡oc⁡K⁡U⁡X=M⁡oc⁡K⁡oc⁡K⁡U⁡X
21 11 5 opococ ⊢K∈OP∧U⁡X∈BaseK→oc⁡K⁡oc⁡K⁡U⁡X=U⁡X
22 9 16 21 syl2anc ⊢K∈HL∧X⊆A→oc⁡K⁡oc⁡K⁡U⁡X=U⁡X
23 22 fveq2d ⊢K∈HL∧X⊆A→M⁡oc⁡K⁡oc⁡K⁡U⁡X=M⁡U⁡X
24 7 20 23 3eqtrd ⊢K∈HL∧X⊆A→⊥˙⁡⊥˙⁡X=M⁡U⁡X