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	$⊢ \underset{˙}{⊥} = oc (K)$
	polat.a	$⊢ A = Atoms (K)$
	polat.m	$⊢ M = pmap (K)$
	polat.p	$⊢ P = ⊥_{𝑃} (K)$
Assertion	polatN	$⊢ (K \in OL \land Q \in A) \to P (\{Q\}) = M (\underset{˙}{⊥} (Q))$

Proof

Step	Hyp	Ref	Expression
1		polat.o	$⊢ \underset{˙}{⊥} = oc (K)$
2		polat.a	$⊢ A = Atoms (K)$
3		polat.m	$⊢ M = pmap (K)$
4		polat.p	$⊢ P = ⊥_{𝑃} (K)$
5		snssi	$⊢ Q \in A \to \{Q\} \subseteq A$
6	1 2 3 4	polvalN	$⊢ (K \in OL \land \{Q\} \subseteq A) \to P (\{Q\}) = A \cap ⋂_{p \in \{Q\}} M (\underset{˙}{⊥} (p))$
7	5 6	sylan2	$⊢ (K \in OL \land Q \in A) \to P (\{Q\}) = A \cap ⋂_{p \in \{Q\}} M (\underset{˙}{⊥} (p))$
8		2fveq3	$⊢ p = Q \to M (\underset{˙}{⊥} (p)) = M (\underset{˙}{⊥} (Q))$
9	8	iinxsng	$⊢ Q \in A \to ⋂_{p \in \{Q\}} M (\underset{˙}{⊥} (p)) = M (\underset{˙}{⊥} (Q))$
10	9	adantl	$⊢ (K \in OL \land Q \in A) \to ⋂_{p \in \{Q\}} M (\underset{˙}{⊥} (p)) = M (\underset{˙}{⊥} (Q))$
11	10	ineq2d	$⊢ (K \in OL \land Q \in A) \to A \cap ⋂_{p \in \{Q\}} M (\underset{˙}{⊥} (p)) = A \cap M (\underset{˙}{⊥} (Q))$
12		olop	$⊢ K \in OL \to K \in OP$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 2	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
15	13 1	opoccl	$⊢ (K \in OP \land Q \in {Base}_{K}) \to \underset{˙}{⊥} (Q) \in {Base}_{K}$
16	12 14 15	syl2an	$⊢ (K \in OL \land Q \in A) \to \underset{˙}{⊥} (Q) \in {Base}_{K}$
17	13 2 3	pmapssat	$⊢ (K \in OL \land \underset{˙}{⊥} (Q) \in {Base}_{K}) \to M (\underset{˙}{⊥} (Q)) \subseteq A$
18	16 17	syldan	$⊢ (K \in OL \land Q \in A) \to M (\underset{˙}{⊥} (Q)) \subseteq A$
19		sseqin2	$⊢ M (\underset{˙}{⊥} (Q)) \subseteq A \leftrightarrow A \cap M (\underset{˙}{⊥} (Q)) = M (\underset{˙}{⊥} (Q))$
20	18 19	sylib	$⊢ (K \in OL \land Q \in A) \to A \cap M (\underset{˙}{⊥} (Q)) = M (\underset{˙}{⊥} (Q))$
21	7 11 20	3eqtrd	$⊢ (K \in OL \land Q \in A) \to P (\{Q\}) = M (\underset{˙}{⊥} (Q))$

Metamath Proof Explorer

Theorem polatN

Proof