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