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 ⁡ K
polat.a ⊢ A = Atoms ⁡ K
polat.m ⊢ M = pmap ⁡ K
polat.p ⊢ P = ⊥ 𝑃 ⁡ K
Assertion polatN ⊢ K ∈ OL ∧ Q ∈ A → P ⁡ Q = M ⁡ ⊥ ˙ ⁡ Q

Proof

Step Hyp Ref Expression
1 polat.o ⊢ ⊥ ˙ = oc ⁡ K
2 polat.a ⊢ A = Atoms ⁡ K
3 polat.m ⊢ M = pmap ⁡ K
4 polat.p ⊢ P = ⊥ 𝑃 ⁡ K
5 snssi ⊢ Q ∈ A → Q ⊆ A
6 1 2 3 4 polvalN ⊢ K ∈ OL ∧ Q ⊆ A → P ⁡ Q = A ∩ ⋂ p ∈ Q M ⁡ ⊥ ˙ ⁡ p
7 5 6 sylan2 ⊢ K ∈ OL ∧ Q ∈ A → P ⁡ Q = A ∩ ⋂ p ∈ Q M ⁡ ⊥ ˙ ⁡ p
8 2fveq3 ⊢ p = Q → M ⁡ ⊥ ˙ ⁡ p = M ⁡ ⊥ ˙ ⁡ Q
9 8 iinxsng ⊢ Q ∈ A → ⋂ p ∈ Q M ⁡ ⊥ ˙ ⁡ p = M ⁡ ⊥ ˙ ⁡ Q
10 9 adantl ⊢ K ∈ OL ∧ Q ∈ A → ⋂ p ∈ Q M ⁡ ⊥ ˙ ⁡ p = M ⁡ ⊥ ˙ ⁡ Q
11 10 ineq2d ⊢ K ∈ OL ∧ Q ∈ A → A ∩ ⋂ p ∈ Q M ⁡ ⊥ ˙ ⁡ p = A ∩ M ⁡ ⊥ ˙ ⁡ Q
12 olop ⊢ K ∈ OL → K ∈ OP
13 eqid ⊢ Base K = Base K
14 13 2 atbase ⊢ Q ∈ A → Q ∈ Base K
15 13 1 opoccl ⊢ K ∈ OP ∧ Q ∈ Base K → ⊥ ˙ ⁡ Q ∈ Base K
16 12 14 15 syl2an ⊢ K ∈ OL ∧ Q ∈ A → ⊥ ˙ ⁡ Q ∈ Base K
17 13 2 3 pmapssat ⊢ K ∈ OL ∧ ⊥ ˙ ⁡ Q ∈ Base K → M ⁡ ⊥ ˙ ⁡ Q ⊆ A
18 16 17 syldan ⊢ K ∈ OL ∧ Q ∈ A → M ⁡ ⊥ ˙ ⁡ Q ⊆ A
19 sseqin2 ⊢ M ⁡ ⊥ ˙ ⁡ Q ⊆ A ↔ A ∩ M ⁡ ⊥ ˙ ⁡ Q = M ⁡ ⊥ ˙ ⁡ Q
20 18 19 sylib ⊢ K ∈ OL ∧ Q ∈ A → A ∩ M ⁡ ⊥ ˙ ⁡ Q = M ⁡ ⊥ ˙ ⁡ Q
21 7 11 20 3eqtrd ⊢ K ∈ OL ∧ Q ∈ A → P ⁡ Q = M ⁡ ⊥ ˙ ⁡ Q