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 ˙ = 𝑃 K
Assertion 2polpmapN K HL X 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 ˙ = 𝑃 K
4 eqid oc K = oc K
5 1 4 2 3 polpmapN K HL X B ˙ M X = M oc K X
6 5 fveq2d K HL X B ˙ ˙ M X = ˙ M oc K X
7 hlop K HL K OP
8 1 4 opoccl K OP X B oc K X B
9 7 8 sylan K HL X B oc K X B
10 1 4 2 3 polpmapN K HL oc K X B ˙ M oc K X = M oc K oc K X
11 9 10 syldan K HL X B ˙ M oc K X = M oc K oc K X
12 1 4 opococ K OP X B oc K oc K X = X
13 7 12 sylan K HL X B oc K oc K X = X
14 13 fveq2d K HL X B M oc K oc K X = M X
15 6 11 14 3eqtrd K HL X B ˙ ˙ M X = M X