Metamath Proof Explorer

Theorem polfvalN

Description: 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 polfvalN ⊢ K ∈ B → P = m ∈ 𝒫 A ⟼ A ∩ ⋂ p ∈ m 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 elex ⊢ K ∈ B → K ∈ V
6 fveq2 ⊢ h = K → Atoms ⁡ h = Atoms ⁡ K
7 6 2 eqtr4di ⊢ h = K → Atoms ⁡ h = A
8 7 pweqd ⊢ h = K → 𝒫 Atoms ⁡ h = 𝒫 A
9 fveq2 ⊢ h = K → pmap ⁡ h = pmap ⁡ K
10 9 3 eqtr4di ⊢ h = K → pmap ⁡ h = M
11 fveq2 ⊢ h = K → oc ⁡ h = oc ⁡ K
12 11 1 eqtr4di ⊢ h = K → oc ⁡ h = ⊥ ˙
13 12 fveq1d ⊢ h = K → oc ⁡ h ⁡ p = ⊥ ˙ ⁡ p
14 10 13 fveq12d ⊢ h = K → pmap ⁡ h ⁡ oc ⁡ h ⁡ p = M ⁡ ⊥ ˙ ⁡ p
15 14 adantr ⊢ h = K ∧ p ∈ m → pmap ⁡ h ⁡ oc ⁡ h ⁡ p = M ⁡ ⊥ ˙ ⁡ p
16 15 iineq2dv ⊢ h = K → ⋂ p ∈ m pmap ⁡ h ⁡ oc ⁡ h ⁡ p = ⋂ p ∈ m M ⁡ ⊥ ˙ ⁡ p
17 7 16 ineq12d ⊢ h = K → Atoms ⁡ h ∩ ⋂ p ∈ m pmap ⁡ h ⁡ oc ⁡ h ⁡ p = A ∩ ⋂ p ∈ m M ⁡ ⊥ ˙ ⁡ p
18 8 17 mpteq12dv ⊢ h = K → m ∈ 𝒫 Atoms ⁡ h ⟼ Atoms ⁡ h ∩ ⋂ p ∈ m pmap ⁡ h ⁡ oc ⁡ h ⁡ p = m ∈ 𝒫 A ⟼ A ∩ ⋂ p ∈ m M ⁡ ⊥ ˙ ⁡ p
19 df-polarityN ⊢ ⊥ 𝑃 = h ∈ V ⟼ m ∈ 𝒫 Atoms ⁡ h ⟼ Atoms ⁡ h ∩ ⋂ p ∈ m pmap ⁡ h ⁡ oc ⁡ h ⁡ p
20 2 fvexi ⊢ A ∈ V
21 20 pwex ⊢ 𝒫 A ∈ V
22 21 mptex ⊢ m ∈ 𝒫 A ⟼ A ∩ ⋂ p ∈ m M ⁡ ⊥ ˙ ⁡ p ∈ V
23 18 19 22 fvmpt ⊢ K ∈ V → ⊥ 𝑃 ⁡ K = m ∈ 𝒫 A ⟼ A ∩ ⋂ p ∈ m M ⁡ ⊥ ˙ ⁡ p
24 4 23 eqtrid ⊢ K ∈ V → P = m ∈ 𝒫 A ⟼ A ∩ ⋂ p ∈ m M ⁡ ⊥ ˙ ⁡ p
25 5 24 syl ⊢ K ∈ B → P = m ∈ 𝒫 A ⟼ A ∩ ⋂ p ∈ m M ⁡ ⊥ ˙ ⁡ p