Metamath Proof Explorer

Theorem islpoldN

Description: Properties that determine a polarity. (Contributed by NM, 26-Nov-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lpolset.v 
|- V = ( Base ` W )
lpolset.s 
|- S = ( LSubSp ` W )
lpolset.z 
|- .0. = ( 0g ` W )
lpolset.a 
|- A = ( LSAtoms ` W )
lpolset.h 
|- H = ( LSHyp ` W )
lpolset.p 
|- P = ( LPol ` W )
islpold.w 
|- ( ph -> W e. X )
islpold.1 
|- ( ph -> ._|_ : ~P V --> S )
islpold.2 
|- ( ph -> ( ._|_ ` V ) = { .0. } )
islpold.3 
|- ( ( ph /\ ( x C_ V /\ y C_ V /\ x C_ y ) ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) )
islpold.4 
|- ( ( ph /\ x e. A ) -> ( ._|_ ` x ) e. H )
islpold.5 
|- ( ( ph /\ x e. A ) -> ( ._|_ ` ( ._|_ ` x ) ) = x )
Assertion islpoldN 
|- ( ph -> ._|_ e. P )

Proof

Step Hyp Ref Expression
1 lpolset.v 
 |-  V = ( Base ` W )
2 lpolset.s 
 |-  S = ( LSubSp ` W )
3 lpolset.z 
 |-  .0. = ( 0g ` W )
4 lpolset.a 
 |-  A = ( LSAtoms ` W )
5 lpolset.h 
 |-  H = ( LSHyp ` W )
6 lpolset.p 
 |-  P = ( LPol ` W )
7 islpold.w 
 |-  ( ph -> W e. X )
8 islpold.1 
 |-  ( ph -> ._|_ : ~P V --> S )
9 islpold.2 
 |-  ( ph -> ( ._|_ ` V ) = { .0. } )
10 islpold.3 
 |-  ( ( ph /\ ( x C_ V /\ y C_ V /\ x C_ y ) ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) )
11 islpold.4 
 |-  ( ( ph /\ x e. A ) -> ( ._|_ ` x ) e. H )
12 islpold.5 
 |-  ( ( ph /\ x e. A ) -> ( ._|_ ` ( ._|_ ` x ) ) = x )
13 10 ex 
 |-  ( ph -> ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) )
14 13 alrimivv 
 |-  ( ph -> A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) )
15 11 12 jca 
 |-  ( ( ph /\ x e. A ) -> ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) )
16 15 ralrimiva 
 |-  ( ph -> A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) )
17 9 14 16 3jca 
 |-  ( ph -> ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) )
18 1 2 3 4 5 6 islpolN 
 |-  ( W e. X -> ( ._|_ e. P <-> ( ._|_ : ~P V --> S /\ ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )
19 7 18 syl 
 |-  ( ph -> ( ._|_ e. P <-> ( ._|_ : ~P V --> S /\ ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )
20 8 17 19 mpbir2and 
 |-  ( ph -> ._|_ e. P )