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	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	2polss.p	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion	3polN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) = ( ⊥ ‘ 𝑆 ) )

Proof

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