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 𝑉 = ( Base ‘ 𝑊 )
lpolf.s 𝑆 = ( LSubSp ‘ 𝑊 )
lpolf.p 𝑃 = ( LPol ‘ 𝑊 )
lpolf.w ( 𝜑𝑊𝑋 )
lpolf.o ( 𝜑𝑃 )
Assertion lpolfN ( 𝜑 : 𝒫 𝑉𝑆 )

Proof

Step Hyp Ref Expression
1 lpolf.v 𝑉 = ( Base ‘ 𝑊 )
2 lpolf.s 𝑆 = ( LSubSp ‘ 𝑊 )
3 lpolf.p 𝑃 = ( LPol ‘ 𝑊 )
4 lpolf.w ( 𝜑𝑊𝑋 )
5 lpolf.o ( 𝜑𝑃 )
6 eqid ( 0g𝑊 ) = ( 0g𝑊 )
7 eqid ( LSAtoms ‘ 𝑊 ) = ( LSAtoms ‘ 𝑊 )
8 eqid ( LSHyp ‘ 𝑊 ) = ( LSHyp ‘ 𝑊 )
9 1 2 6 7 8 3 islpolN ( 𝑊𝑋 → ( 𝑃 ↔ ( : 𝒫 𝑉𝑆 ∧ ( ( 𝑉 ) = { ( 0g𝑊 ) } ∧ ∀ 𝑥𝑦 ( ( 𝑥𝑉𝑦𝑉𝑥𝑦 ) → ( 𝑦 ) ⊆ ( 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑊 ) ( ( 𝑥 ) ∈ ( LSHyp ‘ 𝑊 ) ∧ ( ‘ ( 𝑥 ) ) = 𝑥 ) ) ) ) )
10 4 9 syl ( 𝜑 → ( 𝑃 ↔ ( : 𝒫 𝑉𝑆 ∧ ( ( 𝑉 ) = { ( 0g𝑊 ) } ∧ ∀ 𝑥𝑦 ( ( 𝑥𝑉𝑦𝑉𝑥𝑦 ) → ( 𝑦 ) ⊆ ( 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑊 ) ( ( 𝑥 ) ∈ ( LSHyp ‘ 𝑊 ) ∧ ( ‘ ( 𝑥 ) ) = 𝑥 ) ) ) ) )
11 5 10 mpbid ( 𝜑 → ( : 𝒫 𝑉𝑆 ∧ ( ( 𝑉 ) = { ( 0g𝑊 ) } ∧ ∀ 𝑥𝑦 ( ( 𝑥𝑉𝑦𝑉𝑥𝑦 ) → ( 𝑦 ) ⊆ ( 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑊 ) ( ( 𝑥 ) ∈ ( LSHyp ‘ 𝑊 ) ∧ ( ‘ ( 𝑥 ) ) = 𝑥 ) ) ) )
12 11 simpld ( 𝜑 : 𝒫 𝑉𝑆 )