polvalN

Description: Value of the projective subspace polarity function. (Contributed by NM, 23-Oct-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	polfval.o	$⊢ \underset{˙}{⊥} = oc (K)$
	polfval.a	$⊢ A = Atoms (K)$
	polfval.m	$⊢ M = pmap (K)$
	polfval.p	$⊢ P = ⊥_{𝑃} (K)$
Assertion	polvalN	$⊢ (K \in B \land X \subseteq A) \to P (X) = A \cap ⋂_{p \in X} M (\underset{˙}{⊥} (p))$

Step	Hyp	Ref	Expression
1		polfval.o	$⊢ \underset{˙}{⊥} = oc (K)$
2		polfval.a	$⊢ A = Atoms (K)$
3		polfval.m	$⊢ M = pmap (K)$
4		polfval.p	$⊢ P = ⊥_{𝑃} (K)$
5	2	fvexi	$⊢ A \in V$
6	5	elpw2	$⊢ X \in 𝒫 A \leftrightarrow X \subseteq A$
7	1 2 3 4	polfvalN	$⊢ K \in B \to P = (m \in 𝒫 A ⟼ A \cap ⋂_{p \in m} M (\underset{˙}{⊥} (p)))$
8	7	fveq1d	$⊢ K \in B \to P (X) = (m \in 𝒫 A ⟼ A \cap ⋂_{p \in m} M (\underset{˙}{⊥} (p))) (X)$
9		iineq1	$⊢ m = X \to ⋂_{p \in m} M (\underset{˙}{⊥} (p)) = ⋂_{p \in X} M (\underset{˙}{⊥} (p))$
10	9	ineq2d	$⊢ m = X \to A \cap ⋂_{p \in m} M (\underset{˙}{⊥} (p)) = A \cap ⋂_{p \in X} M (\underset{˙}{⊥} (p))$
11		eqid	$⊢ (m \in 𝒫 A ⟼ A \cap ⋂_{p \in m} M (\underset{˙}{⊥} (p))) = (m \in 𝒫 A ⟼ A \cap ⋂_{p \in m} M (\underset{˙}{⊥} (p)))$
12	5	inex1	$⊢ A \cap ⋂_{p \in X} M (\underset{˙}{⊥} (p)) \in V$
13	10 11 12	fvmpt	$⊢ X \in 𝒫 A \to (m \in 𝒫 A ⟼ A \cap ⋂_{p \in m} M (\underset{˙}{⊥} (p))) (X) = A \cap ⋂_{p \in X} M (\underset{˙}{⊥} (p))$
14	8 13	sylan9eq	$⊢ (K \in B \land X \in 𝒫 A) \to P (X) = A \cap ⋂_{p \in X} M (\underset{˙}{⊥} (p))$
15	6 14	sylan2br	$⊢ (K \in B \land X \subseteq A) \to P (X) = A \cap ⋂_{p \in X} M (\underset{˙}{⊥} (p))$

Metamath Proof Explorer