Theorem 2polpmapN

Description: Double polarity of a projective map. (Contributed by NM, 24-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2polpmap.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	2polpmap.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
	2polpmap.p	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion	2polpmapN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑀 ‘ 𝑋 ) ) ) = ( 𝑀 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		2polpmap.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		2polpmap.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
3		2polpmap.p	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
4		eqid	⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
5	1 4 2 3	polpmapN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑀 ‘ 𝑋 ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
6	5	fveq2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑀 ‘ 𝑋 ) ) ) = ( ⊥ ‘ ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) )
7		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
8	1 4	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
9	7 8	sylan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
10	1 4 2 3	polpmapN	⊢ ( ( 𝐾 ∈ HL ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) )
11	9 10	syldan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) )
12	1 4	opococ	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 )
13	7 12	sylan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 )
14	13	fveq2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) = ( 𝑀 ‘ 𝑋 ) )
15	6 11 14	3eqtrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑀 ‘ 𝑋 ) ) ) = ( 𝑀 ‘ 𝑋 ) )