Metamath Proof Explorer

Theorem 2polpmapN

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

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

Proof

Step Hyp Ref Expression
1 2polpmap.b 
 |-  B = ( Base ` K )
2 2polpmap.m 
 |-  M = ( pmap ` K )
3 2polpmap.p 
 |-  ._|_ = ( _|_P ` K )
4 eqid 
 |-  ( oc ` K ) = ( oc ` K )
5 1 4 2 3 polpmapN 
 |-  ( ( K e. HL /\ X e. B ) -> ( ._|_ ` ( M ` X ) ) = ( M ` ( ( oc ` K ) ` X ) ) )
6 5 fveq2d 
 |-  ( ( K e. HL /\ X e. B ) -> ( ._|_ ` ( ._|_ ` ( M ` X ) ) ) = ( ._|_ ` ( M ` ( ( oc ` K ) ` X ) ) ) )
7 hlop 
 |-  ( K e. HL -> K e. OP )
8 1 4 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` X ) e. B )
9 7 8 sylan 
 |-  ( ( K e. HL /\ X e. B ) -> ( ( oc ` K ) ` X ) e. B )
10 1 4 2 3 polpmapN 
 |-  ( ( K e. HL /\ ( ( oc ` K ) ` X ) e. B ) -> ( ._|_ ` ( M ` ( ( oc ` K ) ` X ) ) ) = ( M ` ( ( oc ` K ) ` ( ( oc ` K ) ` X ) ) ) )
11 9 10 syldan 
 |-  ( ( K e. HL /\ X e. B ) -> ( ._|_ ` ( M ` ( ( oc ` K ) ` X ) ) ) = ( M ` ( ( oc ` K ) ` ( ( oc ` K ) ` X ) ) ) )
12 1 4 opococ 
 |-  ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` ( ( oc ` K ) ` X ) ) = X )
13 7 12 sylan 
 |-  ( ( K e. HL /\ X e. B ) -> ( ( oc ` K ) ` ( ( oc ` K ) ` X ) ) = X )
14 13 fveq2d 
 |-  ( ( K e. HL /\ X e. B ) -> ( M ` ( ( oc ` K ) ` ( ( oc ` K ) ` X ) ) ) = ( M ` X ) )
15 6 11 14 3eqtrd 
 |-  ( ( K e. HL /\ X e. B ) -> ( ._|_ ` ( ._|_ ` ( M ` X ) ) ) = ( M ` X ) )