Metamath Proof Explorer

Theorem lpolsatN

Description: The polarity of an atomic subspace is a hyperplane. (Contributed by NM, 26-Nov-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lpolsat.a 
|- A = ( LSAtoms ` W )
lpolsat.h 
|- H = ( LSHyp ` W )
lpolsat.p 
|- P = ( LPol ` W )
lpolsat.w 
|- ( ph -> W e. X )
lpolsat.o 
|- ( ph -> ._|_ e. P )
lpolsat.q 
|- ( ph -> Q e. A )
Assertion lpolsatN 
|- ( ph -> ( ._|_ ` Q ) e. H )

Proof

Step Hyp Ref Expression
1 lpolsat.a 
 |-  A = ( LSAtoms ` W )
2 lpolsat.h 
 |-  H = ( LSHyp ` W )
3 lpolsat.p 
 |-  P = ( LPol ` W )
4 lpolsat.w 
 |-  ( ph -> W e. X )
5 lpolsat.o 
 |-  ( ph -> ._|_ e. P )
6 lpolsat.q 
 |-  ( ph -> Q e. A )
7 eqid 
 |-  ( Base ` W ) = ( Base ` W )
8 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
9 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
10 7 8 9 1 2 3 islpolN 
 |-  ( W e. X -> ( ._|_ e. P <-> ( ._|_ : ~P ( Base ` W ) --> ( LSubSp ` W ) /\ ( ( ._|_ ` ( Base ` W ) ) = { ( 0g ` W ) } /\ A. x A. y ( ( x C_ ( Base ` W ) /\ y C_ ( Base ` W ) /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )
11 4 10 syl 
 |-  ( ph -> ( ._|_ e. P <-> ( ._|_ : ~P ( Base ` W ) --> ( LSubSp ` W ) /\ ( ( ._|_ ` ( Base ` W ) ) = { ( 0g ` W ) } /\ A. x A. y ( ( x C_ ( Base ` W ) /\ y C_ ( Base ` W ) /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )
12 5 11 mpbid 
 |-  ( ph -> ( ._|_ : ~P ( Base ` W ) --> ( LSubSp ` W ) /\ ( ( ._|_ ` ( Base ` W ) ) = { ( 0g ` W ) } /\ A. x A. y ( ( x C_ ( Base ` W ) /\ y C_ ( Base ` W ) /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) )
13 simpr3 
 |-  ( ( ._|_ : ~P ( Base ` W ) --> ( LSubSp ` W ) /\ ( ( ._|_ ` ( Base ` W ) ) = { ( 0g ` W ) } /\ A. x A. y ( ( x C_ ( Base ` W ) /\ y C_ ( Base ` W ) /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) -> A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) )
14 fveq2 
 |-  ( x = Q -> ( ._|_ ` x ) = ( ._|_ ` Q ) )
15 14 eleq1d 
 |-  ( x = Q -> ( ( ._|_ ` x ) e. H <-> ( ._|_ ` Q ) e. H ) )
16 2fveq3 
 |-  ( x = Q -> ( ._|_ ` ( ._|_ ` x ) ) = ( ._|_ ` ( ._|_ ` Q ) ) )
17 id 
 |-  ( x = Q -> x = Q )
18 16 17 eqeq12d 
 |-  ( x = Q -> ( ( ._|_ ` ( ._|_ ` x ) ) = x <-> ( ._|_ ` ( ._|_ ` Q ) ) = Q ) )
19 15 18 anbi12d 
 |-  ( x = Q -> ( ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) <-> ( ( ._|_ ` Q ) e. H /\ ( ._|_ ` ( ._|_ ` Q ) ) = Q ) ) )
20 19 rspcv 
 |-  ( Q e. A -> ( A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) -> ( ( ._|_ ` Q ) e. H /\ ( ._|_ ` ( ._|_ ` Q ) ) = Q ) ) )
21 6 20 syl 
 |-  ( ph -> ( A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) -> ( ( ._|_ ` Q ) e. H /\ ( ._|_ ` ( ._|_ ` Q ) ) = Q ) ) )
22 simpl 
 |-  ( ( ( ._|_ ` Q ) e. H /\ ( ._|_ ` ( ._|_ ` Q ) ) = Q ) -> ( ._|_ ` Q ) e. H )
23 13 21 22 syl56 
 |-  ( ph -> ( ( ._|_ : ~P ( Base ` W ) --> ( LSubSp ` W ) /\ ( ( ._|_ ` ( Base ` W ) ) = { ( 0g ` W ) } /\ A. x A. y ( ( x C_ ( Base ` W ) /\ y C_ ( Base ` W ) /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) -> ( ._|_ ` Q ) e. H ) )
24 12 23 mpd 
 |-  ( ph -> ( ._|_ ` Q ) e. H )