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	|- ._|_ = ( _|_P ` K )
Assertion	3polN	|- ( ( K e. HL /\ S C_ A ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` S ) ) ) = ( ._|_ ` S ) )

Proof

Step	Hyp	Ref	Expression
1		2polss.a	|- A = ( Atoms ` K )
2		2polss.p	|- ._|_ = ( _|_P ` K )
3		hlclat	|- ( K e. HL -> K e. CLat )
4		eqid	|- ( Base ` K ) = ( Base ` K )
5	4 1	atssbase	|- A C_ ( Base ` K )
6		sstr	|- ( ( S C_ A /\ A C_ ( Base ` K ) ) -> S C_ ( Base ` K ) )
7	5 6	mpan2	|- ( S C_ A -> S C_ ( Base ` K ) )
8		eqid	|- ( lub ` K ) = ( lub ` K )
9	4 8	clatlubcl	|- ( ( K e. CLat /\ S C_ ( Base ` K ) ) -> ( ( lub ` K ) ` S ) e. ( Base ` K ) )
10	3 7 9	syl2an	|- ( ( K e. HL /\ S C_ A ) -> ( ( lub ` K ) ` S ) e. ( Base ` K ) )
11		eqid	|- ( oc ` K ) = ( oc ` K )
12		eqid	|- ( pmap ` K ) = ( pmap ` K )
13	4 11 12 2	polpmapN	|- ( ( K e. HL /\ ( ( lub ` K ) ` S ) e. ( Base ` K ) ) -> ( ._|_ ` ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` S ) ) ) )
14	10 13	syldan	|- ( ( K e. HL /\ S C_ A ) -> ( ._|_ ` ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` S ) ) ) )
15	8 1 12 2	2polvalN	|- ( ( K e. HL /\ S C_ A ) -> ( ._|_ ` ( ._|_ ` S ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) )
16	15	fveq2d	|- ( ( K e. HL /\ S C_ A ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` S ) ) ) = ( ._|_ ` ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) ) )
17	8 11 1 12 2	polval2N	|- ( ( K e. HL /\ S C_ A ) -> ( ._|_ ` S ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` S ) ) ) )
18	14 16 17	3eqtr4d	|- ( ( K e. HL /\ S C_ A ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` S ) ) ) = ( ._|_ ` S ) )