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 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ‘ ( 𝑃 ‘ { 𝑄 } ) ) = { 𝑄 } )