Theorem polatN

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

	Ref	Expression
Hypotheses	polat.o	⊢ ⊥ = ( oc ‘ 𝐾 )
	polat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	polat.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
	polat.p	⊢ 𝑃 = ( ⊥𝑃 ‘ 𝐾 )
Assertion	polatN	⊢ ( ( 𝐾 ∈ OL ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ‘ { 𝑄 } ) = ( 𝑀 ‘ ( ⊥ ‘ 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		polat.o	⊢ ⊥ = ( oc ‘ 𝐾 )
2		polat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		polat.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
4		polat.p	⊢ 𝑃 = ( ⊥𝑃 ‘ 𝐾 )
5		snssi	⊢ ( 𝑄 ∈ 𝐴 → { 𝑄 } ⊆ 𝐴 )
6	1 2 3 4	polvalN	⊢ ( ( 𝐾 ∈ OL ∧ { 𝑄 } ⊆ 𝐴 ) → ( 𝑃 ‘ { 𝑄 } ) = ( 𝐴 ∩ ∩ 𝑝 ∈ { 𝑄 } ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) )
7	5 6	sylan2	⊢ ( ( 𝐾 ∈ OL ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ‘ { 𝑄 } ) = ( 𝐴 ∩ ∩ 𝑝 ∈ { 𝑄 } ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) )
8		2fveq3	⊢ ( 𝑝 = 𝑄 → ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) = ( 𝑀 ‘ ( ⊥ ‘ 𝑄 ) ) )
9	8	iinxsng	⊢ ( 𝑄 ∈ 𝐴 → ∩ 𝑝 ∈ { 𝑄 } ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) = ( 𝑀 ‘ ( ⊥ ‘ 𝑄 ) ) )
10	9	adantl	⊢ ( ( 𝐾 ∈ OL ∧ 𝑄 ∈ 𝐴 ) → ∩ 𝑝 ∈ { 𝑄 } ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) = ( 𝑀 ‘ ( ⊥ ‘ 𝑄 ) ) )
11	10	ineq2d	⊢ ( ( 𝐾 ∈ OL ∧ 𝑄 ∈ 𝐴 ) → ( 𝐴 ∩ ∩ 𝑝 ∈ { 𝑄 } ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) = ( 𝐴 ∩ ( 𝑀 ‘ ( ⊥ ‘ 𝑄 ) ) ) )
12		olop	⊢ ( 𝐾 ∈ OL → 𝐾 ∈ OP )
13		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14	13 2	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
15	13 1	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( ⊥ ‘ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
16	12 14 15	syl2an	⊢ ( ( 𝐾 ∈ OL ∧ 𝑄 ∈ 𝐴 ) → ( ⊥ ‘ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
17	13 2 3	pmapssat	⊢ ( ( 𝐾 ∈ OL ∧ ( ⊥ ‘ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑀 ‘ ( ⊥ ‘ 𝑄 ) ) ⊆ 𝐴 )
18	16 17	syldan	⊢ ( ( 𝐾 ∈ OL ∧ 𝑄 ∈ 𝐴 ) → ( 𝑀 ‘ ( ⊥ ‘ 𝑄 ) ) ⊆ 𝐴 )
19		sseqin2	⊢ ( ( 𝑀 ‘ ( ⊥ ‘ 𝑄 ) ) ⊆ 𝐴 ↔ ( 𝐴 ∩ ( 𝑀 ‘ ( ⊥ ‘ 𝑄 ) ) ) = ( 𝑀 ‘ ( ⊥ ‘ 𝑄 ) ) )
20	18 19	sylib	⊢ ( ( 𝐾 ∈ OL ∧ 𝑄 ∈ 𝐴 ) → ( 𝐴 ∩ ( 𝑀 ‘ ( ⊥ ‘ 𝑄 ) ) ) = ( 𝑀 ‘ ( ⊥ ‘ 𝑄 ) ) )
21	7 11 20	3eqtrd	⊢ ( ( 𝐾 ∈ OL ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ‘ { 𝑄 } ) = ( 𝑀 ‘ ( ⊥ ‘ 𝑄 ) ) )