Metamath Proof Explorer

Theorem 3polN

Description: Triple polarity cancels to a single polarity. (Contributed by NM, 6-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2polss.a ⊢ A = Atoms ⁡ K
2polss.p ⊢ ⊥ ˙ = ⊥ 𝑃 ⁡ K
Assertion 3polN ⊢ K ∈ HL ∧ S ⊆ A → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S = ⊥ ˙ ⁡ S

Proof

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