Metamath Proof Explorer

Theorem lpolsetN

Description: The set of polarities of a left module or left vector space. (Contributed by NM, 24-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 )
Assertion lpolsetN 
|- ( W e. X -> P = { o e. ( S ^m ~P V ) | ( ( o ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. A ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) ) } )

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 elex 
 |-  ( W e. X -> W e. _V )
8 fveq2 
 |-  ( w = W -> ( LSubSp ` w ) = ( LSubSp ` W ) )
9 8 2 eqtr4di 
 |-  ( w = W -> ( LSubSp ` w ) = S )
10 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
11 10 1 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = V )
12 11 pweqd 
 |-  ( w = W -> ~P ( Base ` w ) = ~P V )
13 9 12 oveq12d 
 |-  ( w = W -> ( ( LSubSp ` w ) ^m ~P ( Base ` w ) ) = ( S ^m ~P V ) )
14 11 fveq2d 
 |-  ( w = W -> ( o ` ( Base ` w ) ) = ( o ` V ) )
15 fveq2 
 |-  ( w = W -> ( 0g ` w ) = ( 0g ` W ) )
16 15 3 eqtr4di 
 |-  ( w = W -> ( 0g ` w ) = .0. )
17 16 sneqd 
 |-  ( w = W -> { ( 0g ` w ) } = { .0. } )
18 14 17 eqeq12d 
 |-  ( w = W -> ( ( o ` ( Base ` w ) ) = { ( 0g ` w ) } <-> ( o ` V ) = { .0. } ) )
19 11 sseq2d 
 |-  ( w = W -> ( x C_ ( Base ` w ) <-> x C_ V ) )
20 11 sseq2d 
 |-  ( w = W -> ( y C_ ( Base ` w ) <-> y C_ V ) )
21 19 20 3anbi12d 
 |-  ( w = W -> ( ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y ) <-> ( x C_ V /\ y C_ V /\ x C_ y ) ) )
22 21 imbi1d 
 |-  ( w = W -> ( ( ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) <-> ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) ) )
23 22 2albidv 
 |-  ( w = W -> ( A. x A. y ( ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) <-> A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) ) )
24 fveq2 
 |-  ( w = W -> ( LSAtoms ` w ) = ( LSAtoms ` W ) )
25 24 4 eqtr4di 
 |-  ( w = W -> ( LSAtoms ` w ) = A )
26 fveq2 
 |-  ( w = W -> ( LSHyp ` w ) = ( LSHyp ` W ) )
27 26 5 eqtr4di 
 |-  ( w = W -> ( LSHyp ` w ) = H )
28 27 eleq2d 
 |-  ( w = W -> ( ( o ` x ) e. ( LSHyp ` w ) <-> ( o ` x ) e. H ) )
29 28 anbi1d 
 |-  ( w = W -> ( ( ( o ` x ) e. ( LSHyp ` w ) /\ ( o ` ( o ` x ) ) = x ) <-> ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) ) )
30 25 29 raleqbidv 
 |-  ( w = W -> ( A. x e. ( LSAtoms ` w ) ( ( o ` x ) e. ( LSHyp ` w ) /\ ( o ` ( o ` x ) ) = x ) <-> A. x e. A ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) ) )
31 18 23 30 3anbi123d 
 |-  ( w = W -> ( ( ( o ` ( Base ` w ) ) = { ( 0g ` w ) } /\ A. x A. y ( ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. ( LSAtoms ` w ) ( ( o ` x ) e. ( LSHyp ` w ) /\ ( o ` ( o ` x ) ) = x ) ) <-> ( ( o ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. A ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) ) ) )
32 13 31 rabeqbidv 
 |-  ( w = W -> { o e. ( ( LSubSp ` w ) ^m ~P ( Base ` w ) ) | ( ( o ` ( Base ` w ) ) = { ( 0g ` w ) } /\ A. x A. y ( ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. ( LSAtoms ` w ) ( ( o ` x ) e. ( LSHyp ` w ) /\ ( o ` ( o ` x ) ) = x ) ) } = { o e. ( S ^m ~P V ) | ( ( o ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. A ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) ) } )
33 df-lpolN 
 |-  LPol = ( w e. _V |-> { o e. ( ( LSubSp ` w ) ^m ~P ( Base ` w ) ) | ( ( o ` ( Base ` w ) ) = { ( 0g ` w ) } /\ A. x A. y ( ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. ( LSAtoms ` w ) ( ( o ` x ) e. ( LSHyp ` w ) /\ ( o ` ( o ` x ) ) = x ) ) } )
34 ovex 
 |-  ( S ^m ~P V ) e. _V
35 34 rabex 
 |-  { o e. ( S ^m ~P V ) | ( ( o ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. A ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) ) } e. _V
36 32 33 35 fvmpt 
 |-  ( W e. _V -> ( LPol ` W ) = { o e. ( S ^m ~P V ) | ( ( o ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. A ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) ) } )
37 6 36 syl5eq 
 |-  ( W e. _V -> P = { o e. ( S ^m ~P V ) | ( ( o ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. A ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) ) } )
38 7 37 syl 
 |-  ( W e. X -> P = { o e. ( S ^m ~P V ) | ( ( o ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. A ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) ) } )