Metamath Proof Explorer


Theorem lpolfN

Description: Functionality of a polarity. (Contributed by NM, 26-Nov-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lpolf.v V = Base W
lpolf.s S = LSubSp W
lpolf.p P = LPol W
lpolf.w φ W X
lpolf.o φ ˙ P
Assertion lpolfN φ ˙ : 𝒫 V S

Proof

Step Hyp Ref Expression
1 lpolf.v V = Base W
2 lpolf.s S = LSubSp W
3 lpolf.p P = LPol W
4 lpolf.w φ W X
5 lpolf.o φ ˙ P
6 eqid 0 W = 0 W
7 eqid LSAtoms W = LSAtoms W
8 eqid LSHyp W = LSHyp W
9 1 2 6 7 8 3 islpolN W X ˙ P ˙ : 𝒫 V S ˙ V = 0 W x y x V y V x y ˙ y ˙ x x LSAtoms W ˙ x LSHyp W ˙ ˙ x = x
10 4 9 syl φ ˙ P ˙ : 𝒫 V S ˙ V = 0 W x y x V y V x y ˙ y ˙ x x LSAtoms W ˙ x LSHyp W ˙ ˙ x = x
11 5 10 mpbid φ ˙ : 𝒫 V S ˙ V = 0 W x y x V y V x y ˙ y ˙ x x LSAtoms W ˙ x LSHyp W ˙ ˙ x = x
12 11 simpld φ ˙ : 𝒫 V S