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

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 ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2polat.p ⊢ 𝑃 = ( ⊥𝑃 ‘ 𝐾 )
Assertion 2polatN ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ‘ ( 𝑃 ‘ { 𝑄 } ) ) = { 𝑄 } )

Proof

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