# 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}=\mathrm{lub}\left({K}\right)$
2polval.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
2polval.m ${⊢}{M}=\mathrm{pmap}\left({K}\right)$
2polval.p
Assertion 2polvalN

### Proof

Step Hyp Ref Expression
1 2polval.u ${⊢}{U}=\mathrm{lub}\left({K}\right)$
2 2polval.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 2polval.m ${⊢}{M}=\mathrm{pmap}\left({K}\right)$
4 2polval.p
5 eqid ${⊢}\mathrm{oc}\left({K}\right)=\mathrm{oc}\left({K}\right)$
6 1 5 2 3 4 polval2N
7 6 fveq2d
8 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
9 8 adantr ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\right)\to {K}\in \mathrm{OP}$
10 hlclat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{CLat}$
11 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
12 11 2 atssbase ${⊢}{A}\subseteq {\mathrm{Base}}_{{K}}$
13 sstr ${⊢}\left({X}\subseteq {A}\wedge {A}\subseteq {\mathrm{Base}}_{{K}}\right)\to {X}\subseteq {\mathrm{Base}}_{{K}}$
14 12 13 mpan2 ${⊢}{X}\subseteq {A}\to {X}\subseteq {\mathrm{Base}}_{{K}}$
15 11 1 clatlubcl ${⊢}\left({K}\in \mathrm{CLat}\wedge {X}\subseteq {\mathrm{Base}}_{{K}}\right)\to {U}\left({X}\right)\in {\mathrm{Base}}_{{K}}$
16 10 14 15 syl2an ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\right)\to {U}\left({X}\right)\in {\mathrm{Base}}_{{K}}$
17 11 5 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {U}\left({X}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left({U}\left({X}\right)\right)\in {\mathrm{Base}}_{{K}}$
18 9 16 17 syl2anc ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\right)\to \mathrm{oc}\left({K}\right)\left({U}\left({X}\right)\right)\in {\mathrm{Base}}_{{K}}$
19 11 5 3 4 polpmapN
20 18 19 syldan
21 11 5 opococ ${⊢}\left({K}\in \mathrm{OP}\wedge {U}\left({X}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({U}\left({X}\right)\right)\right)={U}\left({X}\right)$
22 9 16 21 syl2anc ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({U}\left({X}\right)\right)\right)={U}\left({X}\right)$
23 22 fveq2d ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\right)\to {M}\left(\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({U}\left({X}\right)\right)\right)\right)={M}\left({U}\left({X}\right)\right)$
24 7 20 23 3eqtrd