This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psubclsetN

Description: The set of closed projective subspaces in a Hilbert lattice. (Contributed by NM, 23-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses psubclset.a 
|- A = ( Atoms ` K )
psubclset.p 
|- ._|_ = ( _|_P ` K )
psubclset.c 
|- C = ( PSubCl ` K )
Assertion psubclsetN 
|- ( K e. B -> C = { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } )

Proof

Step Hyp Ref Expression
1 psubclset.a 
 |-  A = ( Atoms ` K )
2 psubclset.p 
 |-  ._|_ = ( _|_P ` K )
3 psubclset.c 
 |-  C = ( PSubCl ` K )
4 elex 
 |-  ( K e. B -> K e. _V )
5 fveq2 
 |-  ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
6 5 1 eqtr4di 
 |-  ( k = K -> ( Atoms ` k ) = A )
7 6 sseq2d 
 |-  ( k = K -> ( s C_ ( Atoms ` k ) <-> s C_ A ) )
8 fveq2 
 |-  ( k = K -> ( _|_P ` k ) = ( _|_P ` K ) )
9 8 2 eqtr4di 
 |-  ( k = K -> ( _|_P ` k ) = ._|_ )
10 9 fveq1d 
 |-  ( k = K -> ( ( _|_P ` k ) ` s ) = ( ._|_ ` s ) )
11 9 10 fveq12d 
 |-  ( k = K -> ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = ( ._|_ ` ( ._|_ ` s ) ) )
12 11 eqeq1d 
 |-  ( k = K -> ( ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s <-> ( ._|_ ` ( ._|_ ` s ) ) = s ) )
13 7 12 anbi12d 
 |-  ( k = K -> ( ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s ) <-> ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) ) )
14 13 abbidv 
 |-  ( k = K -> { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s ) } = { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } )
15 df-psubclN 
 |-  PSubCl = ( k e. _V |-> { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s ) } )
16 1 fvexi 
 |-  A e. _V
17 16 pwex 
 |-  ~P A e. _V
18 velpw 
 |-  ( s e. ~P A <-> s C_ A )
19 18 anbi1i 
 |-  ( ( s e. ~P A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) <-> ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) )
20 19 abbii 
 |-  { s | ( s e. ~P A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } = { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) }
21 ssab2 
 |-  { s | ( s e. ~P A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } C_ ~P A
22 20 21 eqsstrri 
 |-  { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } C_ ~P A
23 17 22 ssexi 
 |-  { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } e. _V
24 14 15 23 fvmpt 
 |-  ( K e. _V -> ( PSubCl ` K ) = { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } )
25 3 24 eqtrid 
 |-  ( K e. _V -> C = { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } )
26 4 25 syl 
 |-  ( K e. B -> C = { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } )