Theorem polpmapN

Description: The polarity of a projective map. (Contributed by NM, 24-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	polpmap.b	|- B = ( Base ` K )
	polpmap.o	|- ._|_ = ( oc ` K )
	polpmap.m	|- M = ( pmap ` K )
	polpmap.p	|- P = ( _|_P ` K )
Assertion	polpmapN	|- ( ( K e. HL /\ X e. B ) -> ( P ` ( M ` X ) ) = ( M ` ( ._|_ ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		polpmap.b	|- B = ( Base ` K )
2		polpmap.o	|- ._|_ = ( oc ` K )
3		polpmap.m	|- M = ( pmap ` K )
4		polpmap.p	|- P = ( _|_P ` K )
5		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
6	1 5 3	pmapssat	|- ( ( K e. HL /\ X e. B ) -> ( M ` X ) C_ ( Atoms ` K ) )
7		eqid	|- ( lub ` K ) = ( lub ` K )
8	7 2 5 3 4	polval2N	|- ( ( K e. HL /\ ( M ` X ) C_ ( Atoms ` K ) ) -> ( P ` ( M ` X ) ) = ( M ` ( ._|_ ` ( ( lub ` K ) ` ( M ` X ) ) ) ) )
9	6 8	syldan	|- ( ( K e. HL /\ X e. B ) -> ( P ` ( M ` X ) ) = ( M ` ( ._|_ ` ( ( lub ` K ) ` ( M ` X ) ) ) ) )
10		eqid	|- ( le ` K ) = ( le ` K )
11	1 10 5 3	pmapval	|- ( ( K e. HL /\ X e. B ) -> ( M ` X ) = { p e. ( Atoms ` K ) | p ( le ` K ) X } )
12	11	fveq2d	|- ( ( K e. HL /\ X e. B ) -> ( ( lub ` K ) ` ( M ` X ) ) = ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p ( le ` K ) X } ) )
13		hlomcmat	|- ( K e. HL -> ( K e. OML /\ K e. CLat /\ K e. AtLat ) )
14	1 10 7 5	atlatmstc	|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p ( le ` K ) X } ) = X )
15	13 14	sylan	|- ( ( K e. HL /\ X e. B ) -> ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p ( le ` K ) X } ) = X )
16	12 15	eqtrd	|- ( ( K e. HL /\ X e. B ) -> ( ( lub ` K ) ` ( M ` X ) ) = X )
17	16	fveq2d	|- ( ( K e. HL /\ X e. B ) -> ( ._|_ ` ( ( lub ` K ) ` ( M ` X ) ) ) = ( ._|_ ` X ) )
18	17	fveq2d	|- ( ( K e. HL /\ X e. B ) -> ( M ` ( ._|_ ` ( ( lub ` K ) ` ( M ` X ) ) ) ) = ( M ` ( ._|_ ` X ) ) )
19	9 18	eqtrd	|- ( ( K e. HL /\ X e. B ) -> ( P ` ( M ` X ) ) = ( M ` ( ._|_ ` X ) ) )