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 ⊢ Base K = Base K
12 11 2 atssbase ⊢ A ⊆ Base K
13 sstr ⊢ X ⊆ A ∧ A ⊆ Base K → X ⊆ Base K
14 12 13 mpan2 ⊢ X ⊆ A → X ⊆ Base K
15 11 1 clatlubcl ⊢ K ∈ CLat ∧ X ⊆ Base K → U ⁡ X ∈ Base K
16 10 14 15 syl2an ⊢ K ∈ HL ∧ X ⊆ A → U ⁡ X ∈ Base K
17 11 5 opoccl ⊢ K ∈ OP ∧ U ⁡ X ∈ Base K → oc ⁡ K ⁡ U ⁡ X ∈ Base K
18 9 16 17 syl2anc ⊢ K ∈ HL ∧ X ⊆ A → oc ⁡ K ⁡ U ⁡ X ∈ Base K
19 11 5 3 4 polpmapN ⊢ K ∈ HL ∧ oc ⁡ K ⁡ U ⁡ X ∈ Base K → ⊥ ˙ ⁡ 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 ∈ Base K → 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