Metamath Proof Explorer

Theorem 2polatN

Description: Double polarity of the singleton of an atom (i.e. a point). (Contributed by NM, 25-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2polat.a ⊢ A = Atoms ⁡ K
2polat.p ⊢ P = ⊥ 𝑃 ⁡ K
Assertion 2polatN ⊢ K ∈ HL ∧ Q ∈ A → P ⁡ P ⁡ Q = Q

Proof

Step Hyp Ref Expression
1 2polat.a ⊢ A = Atoms ⁡ K
2 2polat.p ⊢ P = ⊥ 𝑃 ⁡ K
3 hlol ⊢ K ∈ HL → K ∈ OL
4 eqid ⊢ oc ⁡ K = oc ⁡ K
5 eqid ⊢ pmap ⁡ K = pmap ⁡ K
6 4 1 5 2 polatN ⊢ K ∈ OL ∧ Q ∈ A → P ⁡ Q = pmap ⁡ K ⁡ oc ⁡ K ⁡ Q
7 3 6 sylan ⊢ K ∈ HL ∧ Q ∈ A → P ⁡ Q = pmap ⁡ K ⁡ oc ⁡ K ⁡ Q
8 7 fveq2d ⊢ K ∈ HL ∧ Q ∈ A → P ⁡ P ⁡ Q = P ⁡ pmap ⁡ K ⁡ oc ⁡ K ⁡ Q
9 hlop ⊢ K ∈ HL → K ∈ OP
10 eqid ⊢ Base K = Base K
11 10 1 atbase ⊢ Q ∈ A → Q ∈ Base K
12 10 4 opoccl ⊢ K ∈ OP ∧ Q ∈ Base K → oc ⁡ K ⁡ Q ∈ Base K
13 9 11 12 syl2an ⊢ K ∈ HL ∧ Q ∈ A → oc ⁡ K ⁡ Q ∈ Base K
14 10 4 5 2 polpmapN ⊢ K ∈ HL ∧ oc ⁡ K ⁡ Q ∈ Base K → P ⁡ pmap ⁡ K ⁡ oc ⁡ K ⁡ Q = pmap ⁡ K ⁡ oc ⁡ K ⁡ oc ⁡ K ⁡ Q
15 13 14 syldan ⊢ K ∈ HL ∧ Q ∈ A → P ⁡ pmap ⁡ K ⁡ oc ⁡ K ⁡ Q = pmap ⁡ K ⁡ oc ⁡ K ⁡ oc ⁡ K ⁡ Q
16 10 4 opococ ⊢ K ∈ OP ∧ Q ∈ Base K → oc ⁡ K ⁡ oc ⁡ K ⁡ Q = Q
17 9 11 16 syl2an ⊢ K ∈ HL ∧ Q ∈ A → oc ⁡ K ⁡ oc ⁡ K ⁡ Q = Q
18 17 fveq2d ⊢ K ∈ HL ∧ Q ∈ A → pmap ⁡ K ⁡ oc ⁡ K ⁡ oc ⁡ K ⁡ Q = pmap ⁡ K ⁡ Q
19 1 5 pmapat ⊢ K ∈ HL ∧ Q ∈ A → pmap ⁡ K ⁡ Q = Q
20 18 19 eqtrd ⊢ K ∈ HL ∧ Q ∈ A → pmap ⁡ K ⁡ oc ⁡ K ⁡ oc ⁡ K ⁡ Q = Q
21 15 20 eqtrd ⊢ K ∈ HL ∧ Q ∈ A → P ⁡ pmap ⁡ K ⁡ oc ⁡ K ⁡ Q = Q
22 8 21 eqtrd ⊢ K ∈ HL ∧ Q ∈ A → P ⁡ P ⁡ Q = Q