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=\mathrm{Atoms}\left(K\right)$$
	2polss.p	$$⊢\underset{\dot{}}{\perp }={\perp }_{𝑃}\left(K\right)$$
Assertion	3polN	$$⊢\left(K\in \mathrm{HL}\wedge S\subseteq A\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(S\right)\right)\right)=\underset{\dot{}}{\perp }\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		2polss.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		2polss.p	$$⊢\underset{\dot{}}{\perp }={\perp }_{𝑃}\left(K\right)$$
3		hlclat	$$⊢K\in \mathrm{HL}\to K\in \mathrm{CLat}$$
4		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
5	4 1	atssbase	$$⊢A\subseteq {\mathrm{Base}}_K$$
6		sstr	$$⊢\left(S\subseteq A\wedge A\subseteq {\mathrm{Base}}_K\right)\to S\subseteq {\mathrm{Base}}_K$$
7	5 6	mpan2	$$⊢S\subseteq A\to S\subseteq {\mathrm{Base}}_K$$
8		eqid	$$⊢\mathrm{lub}\left(K\right)=\mathrm{lub}\left(K\right)$$
9	4 8	clatlubcl	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq {\mathrm{Base}}_K\right)\to \mathrm{lub}\left(K\right)\left(S\right)\in {\mathrm{Base}}_K$$
10	3 7 9	syl2an	$$⊢\left(K\in \mathrm{HL}\wedge S\subseteq A\right)\to \mathrm{lub}\left(K\right)\left(S\right)\in {\mathrm{Base}}_K$$
11		eqid	$$⊢\mathrm{oc}\left(K\right)=\mathrm{oc}\left(K\right)$$
12		eqid	$$⊢\mathrm{pmap}\left(K\right)=\mathrm{pmap}\left(K\right)$$
13	4 11 12 2	polpmapN	$$⊢\left(K\in \mathrm{HL}\wedge \mathrm{lub}\left(K\right)\left(S\right)\in {\mathrm{Base}}_K\right)\to \underset{\dot{}}{\perp }\left(\mathrm{pmap}\left(K\right)\left(\mathrm{lub}\left(K\right)\left(S\right)\right)\right)=\mathrm{pmap}\left(K\right)\left(\mathrm{oc}\left(K\right)\left(\mathrm{lub}\left(K\right)\left(S\right)\right)\right)$$
14	10 13	syldan	$$⊢\left(K\in \mathrm{HL}\wedge S\subseteq A\right)\to \underset{\dot{}}{\perp }\left(\mathrm{pmap}\left(K\right)\left(\mathrm{lub}\left(K\right)\left(S\right)\right)\right)=\mathrm{pmap}\left(K\right)\left(\mathrm{oc}\left(K\right)\left(\mathrm{lub}\left(K\right)\left(S\right)\right)\right)$$
15	8 1 12 2	2polvalN	$$⊢\left(K\in \mathrm{HL}\wedge S\subseteq A\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(S\right)\right)=\mathrm{pmap}\left(K\right)\left(\mathrm{lub}\left(K\right)\left(S\right)\right)$$
16	15	fveq2d	$$⊢\left(K\in \mathrm{HL}\wedge S\subseteq A\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(S\right)\right)\right)=\underset{\dot{}}{\perp }\left(\mathrm{pmap}\left(K\right)\left(\mathrm{lub}\left(K\right)\left(S\right)\right)\right)$$
17	8 11 1 12 2	polval2N	$$⊢\left(K\in \mathrm{HL}\wedge S\subseteq A\right)\to \underset{\dot{}}{\perp }\left(S\right)=\mathrm{pmap}\left(K\right)\left(\mathrm{oc}\left(K\right)\left(\mathrm{lub}\left(K\right)\left(S\right)\right)\right)$$
18	14 16 17	3eqtr4d	$$⊢\left(K\in \mathrm{HL}\wedge S\subseteq A\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(S\right)\right)\right)=\underset{\dot{}}{\perp }\left(S\right)$$