Metamath Proof Explorer

Theorem lpolvN

Description: The polarity of the whole space is the zero subspace. (Contributed by NM, 26-Nov-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lpolv.v ⊢ V = Base W
lpolv.z ⊢ 0 ˙ = 0 W
lpolv.p ⊢ P = LPol ⁡ W
lpolv.w ⊢ φ → W ∈ X
lpolv.o ⊢ φ → ⊥ ˙ ∈ P
Assertion lpolvN ⊢ φ → ⊥ ˙ ⁡ V = 0 ˙

Proof

Step Hyp Ref Expression
1 lpolv.v ⊢ V = Base W
2 lpolv.z ⊢ 0 ˙ = 0 W
3 lpolv.p ⊢ P = LPol ⁡ W
4 lpolv.w ⊢ φ → W ∈ X
5 lpolv.o ⊢ φ → ⊥ ˙ ∈ P
6 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
7 eqid ⊢ LSAtoms ⁡ W = LSAtoms ⁡ W
8 eqid ⊢ LSHyp ⁡ W = LSHyp ⁡ W
9 1 6 2 7 8 3 islpolN ⊢ W ∈ X → ⊥ ˙ ∈ P ↔ ⊥ ˙ : 𝒫 V ⟶ LSubSp ⁡ W ∧ ⊥ ˙ ⁡ V = 0 ˙ ∧ ∀ x ∀ y x ⊆ V ∧ y ⊆ V ∧ x ⊆ y → ⊥ ˙ ⁡ y ⊆ ⊥ ˙ ⁡ x ∧ ∀ x ∈ LSAtoms ⁡ W ⊥ ˙ ⁡ x ∈ LSHyp ⁡ W ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ x = x
10 4 9 syl ⊢ φ → ⊥ ˙ ∈ P ↔ ⊥ ˙ : 𝒫 V ⟶ LSubSp ⁡ W ∧ ⊥ ˙ ⁡ V = 0 ˙ ∧ ∀ x ∀ y x ⊆ V ∧ y ⊆ V ∧ x ⊆ y → ⊥ ˙ ⁡ y ⊆ ⊥ ˙ ⁡ x ∧ ∀ x ∈ LSAtoms ⁡ W ⊥ ˙ ⁡ x ∈ LSHyp ⁡ W ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ x = x
11 5 10 mpbid ⊢ φ → ⊥ ˙ : 𝒫 V ⟶ LSubSp ⁡ W ∧ ⊥ ˙ ⁡ V = 0 ˙ ∧ ∀ x ∀ y x ⊆ V ∧ y ⊆ V ∧ x ⊆ y → ⊥ ˙ ⁡ y ⊆ ⊥ ˙ ⁡ x ∧ ∀ x ∈ LSAtoms ⁡ W ⊥ ˙ ⁡ x ∈ LSHyp ⁡ W ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ x = x
12 simpr1 ⊢ ⊥ ˙ : 𝒫 V ⟶ LSubSp ⁡ W ∧ ⊥ ˙ ⁡ V = 0 ˙ ∧ ∀ x ∀ y x ⊆ V ∧ y ⊆ V ∧ x ⊆ y → ⊥ ˙ ⁡ y ⊆ ⊥ ˙ ⁡ x ∧ ∀ x ∈ LSAtoms ⁡ W ⊥ ˙ ⁡ x ∈ LSHyp ⁡ W ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ x = x → ⊥ ˙ ⁡ V = 0 ˙
13 11 12 syl ⊢ φ → ⊥ ˙ ⁡ V = 0 ˙