This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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