Metamath Proof Explorer

Theorem hlhillcs

Description: The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase is applied over and over to conclusion rather than applied once to antecedent - would compressed proof be shorter if applied once to antecedent? (Contributed by NM, 23-Jun-2015)

Ref Expression
Hypotheses hlhillcs.h 
|- H = ( LHyp ` K )
hlhillcs.i 
|- I = ( ( DIsoH ` K ) ` W )
hlhillcs.u 
|- U = ( ( HLHil ` K ) ` W )
hlhillcs.c 
|- C = ( ClSubSp ` U )
hlhillcs.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion hlhillcs 
|- ( ph -> C = ran I )

Proof

Step Hyp Ref Expression
1 hlhillcs.h 
 |-  H = ( LHyp ` K )
2 hlhillcs.i 
 |-  I = ( ( DIsoH ` K ) ` W )
3 hlhillcs.u 
 |-  U = ( ( HLHil ` K ) ` W )
4 hlhillcs.c 
 |-  C = ( ClSubSp ` U )
5 hlhillcs.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
6 3 fvexi 
 |-  U e. _V
7 eqid 
 |-  ( ocv ` U ) = ( ocv ` U )
8 7 4 iscss 
 |-  ( U e. _V -> ( x e. C <-> x = ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) ) )
9 6 8 mp1i 
 |-  ( ph -> ( x e. C <-> x = ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) ) )
10 9 biimpa 
 |-  ( ( ph /\ x e. C ) -> x = ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) )
11 eqid 
 |-  ( Base ` U ) = ( Base ` U )
12 11 4 cssss 
 |-  ( x e. C -> x C_ ( Base ` U ) )
13 eqid 
 |-  ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
14 eqid 
 |-  ( Base ` ( ( DVecH ` K ) ` W ) ) = ( Base ` ( ( DVecH ` K ) ` W ) )
15 eqid 
 |-  ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
16 5 adantr 
 |-  ( ( ph /\ x C_ ( Base ` U ) ) -> ( K e. HL /\ W e. H ) )
17 1 3 5 13 14 hlhilbase 
 |-  ( ph -> ( Base ` ( ( DVecH ` K ) ` W ) ) = ( Base ` U ) )
18 17 sseq2d 
 |-  ( ph -> ( x C_ ( Base ` ( ( DVecH ` K ) ` W ) ) <-> x C_ ( Base ` U ) ) )
19 18 biimpar 
 |-  ( ( ph /\ x C_ ( Base ` U ) ) -> x C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
20 1 2 13 14 15 16 19 dochoccl 
 |-  ( ( ph /\ x C_ ( Base ` U ) ) -> ( x e. ran I <-> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) = x ) )
21 eqcom 
 |-  ( x = ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) <-> ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) = x )
22 1 13 3 16 14 15 7 19 hlhilocv 
 |-  ( ( ph /\ x C_ ( Base ` U ) ) -> ( ( ocv ` U ) ` x ) = ( ( ( ocH ` K ) ` W ) ` x ) )
23 22 fveq2d 
 |-  ( ( ph /\ x C_ ( Base ` U ) ) -> ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) = ( ( ocv ` U ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) )
24 1 13 14 15 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x C_ ( Base ` ( ( DVecH ` K ) ` W ) ) ) -> ( ( ( ocH ` K ) ` W ) ` x ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
25 16 19 24 syl2anc 
 |-  ( ( ph /\ x C_ ( Base ` U ) ) -> ( ( ( ocH ` K ) ` W ) ` x ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
26 1 13 3 16 14 15 7 25 hlhilocv 
 |-  ( ( ph /\ x C_ ( Base ` U ) ) -> ( ( ocv ` U ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) )
27 23 26 eqtrd 
 |-  ( ( ph /\ x C_ ( Base ` U ) ) -> ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) )
28 27 eqeq1d 
 |-  ( ( ph /\ x C_ ( Base ` U ) ) -> ( ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) = x <-> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) = x ) )
29 21 28 syl5bb 
 |-  ( ( ph /\ x C_ ( Base ` U ) ) -> ( x = ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) <-> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) = x ) )
30 20 29 bitr4d 
 |-  ( ( ph /\ x C_ ( Base ` U ) ) -> ( x e. ran I <-> x = ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) ) )
31 12 30 sylan2 
 |-  ( ( ph /\ x e. C ) -> ( x e. ran I <-> x = ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) ) )
32 10 31 mpbird 
 |-  ( ( ph /\ x e. C ) -> x e. ran I )
33 simpr 
 |-  ( ( ph /\ x e. ran I ) -> x e. ran I )
34 5 adantr 
 |-  ( ( ph /\ x e. ran I ) -> ( K e. HL /\ W e. H ) )
35 1 13 2 14 dihrnss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ran I ) -> x C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
36 5 35 sylan 
 |-  ( ( ph /\ x e. ran I ) -> x C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
37 1 13 3 34 14 15 7 36 hlhilocv 
 |-  ( ( ph /\ x e. ran I ) -> ( ( ocv ` U ) ` x ) = ( ( ( ocH ` K ) ` W ) ` x ) )
38 37 fveq2d 
 |-  ( ( ph /\ x e. ran I ) -> ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) = ( ( ocv ` U ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) )
39 34 36 24 syl2anc 
 |-  ( ( ph /\ x e. ran I ) -> ( ( ( ocH ` K ) ` W ) ` x ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
40 1 13 3 34 14 15 7 39 hlhilocv 
 |-  ( ( ph /\ x e. ran I ) -> ( ( ocv ` U ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) )
41 38 40 eqtrd 
 |-  ( ( ph /\ x e. ran I ) -> ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) )
42 41 eqeq1d 
 |-  ( ( ph /\ x e. ran I ) -> ( ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) = x <-> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) = x ) )
43 42 biimpar 
 |-  ( ( ( ph /\ x e. ran I ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) = x ) -> ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) = x )
44 43 eqcomd 
 |-  ( ( ( ph /\ x e. ran I ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) = x ) -> x = ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) )
45 44 ex 
 |-  ( ( ph /\ x e. ran I ) -> ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) = x -> x = ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) ) )
46 1 2 13 14 15 34 36 dochoccl 
 |-  ( ( ph /\ x e. ran I ) -> ( x e. ran I <-> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) = x ) )
47 6 8 mp1i 
 |-  ( ( ph /\ x e. ran I ) -> ( x e. C <-> x = ( ( ocv ` U ) ` ( ( ocv ` U ) ` x ) ) ) )
48 45 46 47 3imtr4d 
 |-  ( ( ph /\ x e. ran I ) -> ( x e. ran I -> x e. C ) )
49 33 48 mpd 
 |-  ( ( ph /\ x e. ran I ) -> x e. C )
50 32 49 impbida 
 |-  ( ph -> ( x e. C <-> x e. ran I ) )
51 50 eqrdv 
 |-  ( ph -> C = ran I )