Metamath Proof Explorer

Theorem polvalN

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

Ref Expression
Hypotheses polfval.o ⊢ ⊥ ˙ = oc ⁡ K
polfval.a ⊢ A = Atoms ⁡ K
polfval.m ⊢ M = pmap ⁡ K
polfval.p ⊢ P = ⊥ 𝑃 ⁡ K
Assertion polvalN ⊢ K ∈ B ∧ X ⊆ A → P ⁡ X = A ∩ ⋂ p ∈ X M ⁡ ⊥ ˙ ⁡ p

Proof

Step Hyp Ref Expression
1 polfval.o ⊢ ⊥ ˙ = oc ⁡ K
2 polfval.a ⊢ A = Atoms ⁡ K
3 polfval.m ⊢ M = pmap ⁡ K
4 polfval.p ⊢ P = ⊥ 𝑃 ⁡ K
5 2 fvexi ⊢ A ∈ V
6 5 elpw2 ⊢ X ∈ 𝒫 A ↔ X ⊆ A
7 1 2 3 4 polfvalN ⊢ K ∈ B → P = m ∈ 𝒫 A ⟼ A ∩ ⋂ p ∈ m M ⁡ ⊥ ˙ ⁡ p
8 7 fveq1d ⊢ K ∈ B → P ⁡ X = m ∈ 𝒫 A ⟼ A ∩ ⋂ p ∈ m M ⁡ ⊥ ˙ ⁡ p ⁡ X
9 iineq1 ⊢ m = X → ⋂ p ∈ m M ⁡ ⊥ ˙ ⁡ p = ⋂ p ∈ X M ⁡ ⊥ ˙ ⁡ p
10 9 ineq2d ⊢ m = X → A ∩ ⋂ p ∈ m M ⁡ ⊥ ˙ ⁡ p = A ∩ ⋂ p ∈ X M ⁡ ⊥ ˙ ⁡ p
11 eqid ⊢ m ∈ 𝒫 A ⟼ A ∩ ⋂ p ∈ m M ⁡ ⊥ ˙ ⁡ p = m ∈ 𝒫 A ⟼ A ∩ ⋂ p ∈ m M ⁡ ⊥ ˙ ⁡ p
12 5 inex1 ⊢ A ∩ ⋂ p ∈ X M ⁡ ⊥ ˙ ⁡ p ∈ V
13 10 11 12 fvmpt ⊢ X ∈ 𝒫 A → m ∈ 𝒫 A ⟼ A ∩ ⋂ p ∈ m M ⁡ ⊥ ˙ ⁡ p ⁡ X = A ∩ ⋂ p ∈ X M ⁡ ⊥ ˙ ⁡ p
14 8 13 sylan9eq ⊢ K ∈ B ∧ X ∈ 𝒫 A → P ⁡ X = A ∩ ⋂ p ∈ X M ⁡ ⊥ ˙ ⁡ p
15 6 14 sylan2br ⊢ K ∈ B ∧ X ⊆ A → P ⁡ X = A ∩ ⋂ p ∈ X M ⁡ ⊥ ˙ ⁡ p