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∈mM⁡⊥˙⁡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∈mpmap⁡h⁡oc⁡h⁡p=⋂p∈mM⁡⊥˙⁡p
17 7 16 ineq12d ⊢h=K→Atoms⁡h∩⋂p∈mpmap⁡h⁡oc⁡h⁡p=A∩⋂p∈mM⁡⊥˙⁡p
18 8 17 mpteq12dv ⊢h=K→m∈𝒫Atoms⁡h⟼Atoms⁡h∩⋂p∈mpmap⁡h⁡oc⁡h⁡p=m∈𝒫A⟼A∩⋂p∈mM⁡⊥˙⁡p
19 df-polarityN ⊢⊥𝑃=h∈V⟼m∈𝒫Atoms⁡h⟼Atoms⁡h∩⋂p∈mpmap⁡h⁡oc⁡h⁡p
20 2 fvexi ⊢A∈V
21 20 pwex ⊢𝒫A∈V
22 21 mptex ⊢m∈𝒫A⟼A∩⋂p∈mM⁡⊥˙⁡p∈V
23 18 19 22 fvmpt ⊢K∈V→⊥𝑃⁡K=m∈𝒫A⟼A∩⋂p∈mM⁡⊥˙⁡p
24 4 23 eqtrid ⊢K∈V→P=m∈𝒫A⟼A∩⋂p∈mM⁡⊥˙⁡p
25 5 24 syl ⊢K∈B→P=m∈𝒫A⟼A∩⋂p∈mM⁡⊥˙⁡p