This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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