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 syl5eq K V P = m 𝒫 A A p m M ˙ p
25 5 24 syl K B P = m 𝒫 A A p m M ˙ p