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

Metamath Proof Explorer

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