Metamath Proof Explorer

Theorem psubspset

Description: The set of projective subspaces in a Hilbert lattice. (Contributed by NM, 2-Oct-2011)

Ref Expression
Hypotheses psubspset.l 
|- .<_ = ( le ` K )
psubspset.j 
|- .\/ = ( join ` K )
psubspset.a 
|- A = ( Atoms ` K )
psubspset.s 
|- S = ( PSubSp ` K )
Assertion psubspset 
|- ( K e. B -> S = { s | ( s C_ A /\ A. p e. s A. q e. s A. r e. A ( r .<_ ( p .\/ q ) -> r e. s ) ) } )

Proof

Step Hyp Ref Expression
1 psubspset.l 
 |-  .<_ = ( le ` K )
2 psubspset.j 
 |-  .\/ = ( join ` K )
3 psubspset.a 
 |-  A = ( Atoms ` K )
4 psubspset.s 
 |-  S = ( PSubSp ` K )
5 elex 
 |-  ( K e. B -> K e. _V )
6 fveq2 
 |-  ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
7 6 3 eqtr4di 
 |-  ( k = K -> ( Atoms ` k ) = A )
8 7 sseq2d 
 |-  ( k = K -> ( s C_ ( Atoms ` k ) <-> s C_ A ) )
9 fveq2 
 |-  ( k = K -> ( join ` k ) = ( join ` K ) )
10 9 2 eqtr4di 
 |-  ( k = K -> ( join ` k ) = .\/ )
11 10 oveqd 
 |-  ( k = K -> ( p ( join ` k ) q ) = ( p .\/ q ) )
12 11 breq2d 
 |-  ( k = K -> ( r ( le ` k ) ( p ( join ` k ) q ) <-> r ( le ` k ) ( p .\/ q ) ) )
13 fveq2 
 |-  ( k = K -> ( le ` k ) = ( le ` K ) )
14 13 1 eqtr4di 
 |-  ( k = K -> ( le ` k ) = .<_ )
15 14 breqd 
 |-  ( k = K -> ( r ( le ` k ) ( p .\/ q ) <-> r .<_ ( p .\/ q ) ) )
16 12 15 bitrd 
 |-  ( k = K -> ( r ( le ` k ) ( p ( join ` k ) q ) <-> r .<_ ( p .\/ q ) ) )
17 16 imbi1d 
 |-  ( k = K -> ( ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s ) <-> ( r .<_ ( p .\/ q ) -> r e. s ) ) )
18 7 17 raleqbidv 
 |-  ( k = K -> ( A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s ) <-> A. r e. A ( r .<_ ( p .\/ q ) -> r e. s ) ) )
19 18 2ralbidv 
 |-  ( k = K -> ( A. p e. s A. q e. s A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s ) <-> A. p e. s A. q e. s A. r e. A ( r .<_ ( p .\/ q ) -> r e. s ) ) )
20 8 19 anbi12d 
 |-  ( k = K -> ( ( s C_ ( Atoms ` k ) /\ A. p e. s A. q e. s A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s ) ) <-> ( s C_ A /\ A. p e. s A. q e. s A. r e. A ( r .<_ ( p .\/ q ) -> r e. s ) ) ) )
21 20 abbidv 
 |-  ( k = K -> { s | ( s C_ ( Atoms ` k ) /\ A. p e. s A. q e. s A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s ) ) } = { s | ( s C_ A /\ A. p e. s A. q e. s A. r e. A ( r .<_ ( p .\/ q ) -> r e. s ) ) } )
22 df-psubsp 
 |-  PSubSp = ( k e. _V |-> { s | ( s C_ ( Atoms ` k ) /\ A. p e. s A. q e. s A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s ) ) } )
23 3 fvexi 
 |-  A e. _V
24 23 pwex 
 |-  ~P A e. _V
25 velpw 
 |-  ( s e. ~P A <-> s C_ A )
26 25 anbi1i 
 |-  ( ( s e. ~P A /\ A. p e. s A. q e. s A. r e. A ( r .<_ ( p .\/ q ) -> r e. s ) ) <-> ( s C_ A /\ A. p e. s A. q e. s A. r e. A ( r .<_ ( p .\/ q ) -> r e. s ) ) )
27 26 abbii 
 |-  { s | ( s e. ~P A /\ A. p e. s A. q e. s A. r e. A ( r .<_ ( p .\/ q ) -> r e. s ) ) } = { s | ( s C_ A /\ A. p e. s A. q e. s A. r e. A ( r .<_ ( p .\/ q ) -> r e. s ) ) }
28 ssab2 
 |-  { s | ( s e. ~P A /\ A. p e. s A. q e. s A. r e. A ( r .<_ ( p .\/ q ) -> r e. s ) ) } C_ ~P A
29 27 28 eqsstrri 
 |-  { s | ( s C_ A /\ A. p e. s A. q e. s A. r e. A ( r .<_ ( p .\/ q ) -> r e. s ) ) } C_ ~P A
30 24 29 ssexi 
 |-  { s | ( s C_ A /\ A. p e. s A. q e. s A. r e. A ( r .<_ ( p .\/ q ) -> r e. s ) ) } e. _V
31 21 22 30 fvmpt 
 |-  ( K e. _V -> ( PSubSp ` K ) = { s | ( s C_ A /\ A. p e. s A. q e. s A. r e. A ( r .<_ ( p .\/ q ) -> r e. s ) ) } )
32 4 31 syl5eq 
 |-  ( K e. _V -> S = { s | ( s C_ A /\ A. p e. s A. q e. s A. r e. A ( r .<_ ( p .\/ q ) -> r e. s ) ) } )
33 5 32 syl 
 |-  ( K e. B -> S = { s | ( s C_ A /\ A. p e. s A. q e. s A. r e. A ( r .<_ ( p .\/ q ) -> r e. s ) ) } )