Theorem 2pmaplubN

Description: Double projective map of an LUB. (Contributed by NM, 6-Mar-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sspmaplub.u	|- U = ( lub ` K )
	sspmaplub.a	|- A = ( Atoms ` K )
	sspmaplub.m	|- M = ( pmap ` K )
Assertion	2pmaplubN	|- ( ( K e. HL /\ S C_ A ) -> ( M ` ( U ` ( M ` ( U ` S ) ) ) ) = ( M ` ( U ` S ) ) )

Proof

Step	Hyp	Ref	Expression
1		sspmaplub.u	|- U = ( lub ` K )
2		sspmaplub.a	|- A = ( Atoms ` K )
3		sspmaplub.m	|- M = ( pmap ` K )
4		eqid	|- ( _|_P ` K ) = ( _|_P ` K )
5	1 2 3 4	2polvalN	|- ( ( K e. HL /\ S C_ A ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` S ) ) = ( M ` ( U ` S ) ) )
6	5	fveq2d	|- ( ( K e. HL /\ S C_ A ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` S ) ) ) = ( ( _|_P ` K ) ` ( M ` ( U ` S ) ) ) )
7	6	fveq2d	|- ( ( K e. HL /\ S C_ A ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` S ) ) ) ) = ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` ( U ` S ) ) ) ) )
8	2 4	polssatN	|- ( ( K e. HL /\ S C_ A ) -> ( ( _|_P ` K ) ` S ) C_ A )
9	2 4	3polN	|- ( ( K e. HL /\ ( ( _|_P ` K ) ` S ) C_ A ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` S ) ) ) ) = ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` S ) ) )
10	8 9	syldan	|- ( ( K e. HL /\ S C_ A ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` S ) ) ) ) = ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` S ) ) )
11	7 10	eqtr3d	|- ( ( K e. HL /\ S C_ A ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` ( U ` S ) ) ) ) = ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` S ) ) )
12		hlclat	|- ( K e. HL -> K e. CLat )
13		eqid	|- ( Base ` K ) = ( Base ` K )
14	13 2	atssbase	|- A C_ ( Base ` K )
15		sstr	|- ( ( S C_ A /\ A C_ ( Base ` K ) ) -> S C_ ( Base ` K ) )
16	14 15	mpan2	|- ( S C_ A -> S C_ ( Base ` K ) )
17	13 1	clatlubcl	|- ( ( K e. CLat /\ S C_ ( Base ` K ) ) -> ( U ` S ) e. ( Base ` K ) )
18	12 16 17	syl2an	|- ( ( K e. HL /\ S C_ A ) -> ( U ` S ) e. ( Base ` K ) )
19	13 2 3	pmapssat	|- ( ( K e. HL /\ ( U ` S ) e. ( Base ` K ) ) -> ( M ` ( U ` S ) ) C_ A )
20	18 19	syldan	|- ( ( K e. HL /\ S C_ A ) -> ( M ` ( U ` S ) ) C_ A )
21	1 2 3 4	2polvalN	|- ( ( K e. HL /\ ( M ` ( U ` S ) ) C_ A ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` ( U ` S ) ) ) ) = ( M ` ( U ` ( M ` ( U ` S ) ) ) ) )
22	20 21	syldan	|- ( ( K e. HL /\ S C_ A ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` ( U ` S ) ) ) ) = ( M ` ( U ` ( M ` ( U ` S ) ) ) ) )
23	11 22	eqtr3d	|- ( ( K e. HL /\ S C_ A ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` S ) ) = ( M ` ( U ` ( M ` ( U ` S ) ) ) ) )
24	23 5	eqtr3d	|- ( ( K e. HL /\ S C_ A ) -> ( M ` ( U ` ( M ` ( U ` S ) ) ) ) = ( M ` ( U ` S ) ) )