Metamath Proof Explorer

Theorem lpolpolsatN

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

Ref Expression
Hypotheses lpolpolsat.a 
|- A = ( LSAtoms ` W )
lpolpolsat.p 
|- P = ( LPol ` W )
lpolpolsat.w 
|- ( ph -> W e. X )
lpolpolsat.o 
|- ( ph -> ._|_ e. P )
lpolpolsat.q 
|- ( ph -> Q e. A )
Assertion lpolpolsatN 
|- ( ph -> ( ._|_ ` ( ._|_ ` Q ) ) = Q )

Proof

Step Hyp Ref Expression
1 lpolpolsat.a 
 |-  A = ( LSAtoms ` W )
2 lpolpolsat.p 
 |-  P = ( LPol ` W )
3 lpolpolsat.w 
 |-  ( ph -> W e. X )
4 lpolpolsat.o 
 |-  ( ph -> ._|_ e. P )
5 lpolpolsat.q 
 |-  ( ph -> Q e. A )
6 eqid 
 |-  ( Base ` W ) = ( Base ` W )
7 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
8 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
9 eqid 
 |-  ( LSHyp ` W ) = ( LSHyp ` W )
10 6 7 8 1 9 2 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. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )
11 3 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. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )
12 4 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. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` 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. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) -> A. x e. A ( ( ._|_ ` x ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) )
14 fveq2 
 |-  ( x = Q -> ( ._|_ ` x ) = ( ._|_ ` Q ) )
15 14 eleq1d 
 |-  ( x = Q -> ( ( ._|_ ` x ) e. ( LSHyp ` W ) <-> ( ._|_ ` Q ) e. ( LSHyp ` W ) ) )
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. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) <-> ( ( ._|_ ` Q ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` Q ) ) = Q ) ) )
20 19 rspcv 
 |-  ( Q e. A -> ( A. x e. A ( ( ._|_ ` x ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) -> ( ( ._|_ ` Q ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` Q ) ) = Q ) ) )
21 5 20 syl 
 |-  ( ph -> ( A. x e. A ( ( ._|_ ` x ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) -> ( ( ._|_ ` Q ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` Q ) ) = Q ) ) )
22 simpr 
 |-  ( ( ( ._|_ ` Q ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` Q ) ) = Q ) -> ( ._|_ ` ( ._|_ ` Q ) ) = Q )
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. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) -> ( ._|_ ` ( ._|_ ` Q ) ) = Q ) )
24 12 23 mpd 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` Q ) ) = Q )