Metamath Proof Explorer


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 ) ) )