Metamath Proof Explorer


Theorem pol0N

Description: The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011) (New usage is discouraged.)

Ref Expression
Hypotheses polssat.a A = Atoms K
polssat.p ˙ = 𝑃 K
Assertion pol0N K B ˙ = A

Proof

Step Hyp Ref Expression
1 polssat.a A = Atoms K
2 polssat.p ˙ = 𝑃 K
3 0ss A
4 eqid oc K = oc K
5 eqid pmap K = pmap K
6 4 1 5 2 polvalN K B A ˙ = A p pmap K oc K p
7 3 6 mpan2 K B ˙ = A p pmap K oc K p
8 0iin p pmap K oc K p = V
9 8 ineq2i A p pmap K oc K p = A V
10 inv1 A V = A
11 9 10 eqtri A p pmap K oc K p = A
12 7 11 eqtrdi K B ˙ = A