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. = ( 0g ` W )
lpolv.p 
|- P = ( LPol ` W )
lpolv.w 
|- ( ph -> W e. X )
lpolv.o 
|- ( ph -> ._|_ e. P )
Assertion lpolvN 
|- ( ph -> ( ._|_ ` V ) = { .0. } )

Proof

Step Hyp Ref Expression
1 lpolv.v 
 |-  V = ( Base ` W )
2 lpolv.z 
 |-  .0. = ( 0g ` W )
3 lpolv.p 
 |-  P = ( LPol ` W )
4 lpolv.w 
 |-  ( ph -> W e. X )
5 lpolv.o 
 |-  ( ph -> ._|_ e. 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 e. X -> ( ._|_ e. P <-> ( ._|_ : ~P V --> ( LSubSp ` W ) /\ ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. ( LSAtoms ` W ) ( ( ._|_ ` x ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )
10 4 9 syl 
 |-  ( ph -> ( ._|_ e. P <-> ( ._|_ : ~P V --> ( LSubSp ` W ) /\ ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. ( LSAtoms ` W ) ( ( ._|_ ` x ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )
11 5 10 mpbid 
 |-  ( ph -> ( ._|_ : ~P V --> ( LSubSp ` W ) /\ ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. ( LSAtoms ` W ) ( ( ._|_ ` x ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) )
12 simpr1 
 |-  ( ( ._|_ : ~P V --> ( LSubSp ` W ) /\ ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. ( LSAtoms ` W ) ( ( ._|_ ` x ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) -> ( ._|_ ` V ) = { .0. } )
13 11 12 syl 
 |-  ( ph -> ( ._|_ ` V ) = { .0. } )