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 φ K HL W H
Assertion hlhillcs φ 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 φ K HL W H
6 3 fvexi U V
7 eqid ocv U = ocv U
8 7 4 iscss U V x C x = ocv U ocv U x
9 6 8 mp1i φ x C x = ocv U ocv U x
10 9 biimpa φ x C x = ocv U ocv U x
11 eqid Base U = Base U
12 11 4 cssss x C x 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 φ x Base U K HL W H
17 1 3 5 13 14 hlhilbase φ Base DVecH K W = Base U
18 17 sseq2d φ x Base DVecH K W x Base U
19 18 biimpar φ x Base U x Base DVecH K W
20 1 2 13 14 15 16 19 dochoccl φ x Base U x 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 φ x Base U ocv U x = ocH K W x
23 22 fveq2d φ x Base U ocv U ocv U x = ocv U ocH K W x
24 1 13 14 15 dochssv K HL W H x Base DVecH K W ocH K W x Base DVecH K W
25 16 19 24 syl2anc φ x Base U ocH K W x Base DVecH K W
26 1 13 3 16 14 15 7 25 hlhilocv φ x Base U ocv U ocH K W x = ocH K W ocH K W x
27 23 26 eqtrd φ x Base U ocv U ocv U x = ocH K W ocH K W x
28 27 eqeq1d φ x Base U ocv U ocv U x = x ocH K W ocH K W x = x
29 21 28 syl5bb φ x Base U x = ocv U ocv U x ocH K W ocH K W x = x
30 20 29 bitr4d φ x Base U x ran I x = ocv U ocv U x
31 12 30 sylan2 φ x C x ran I x = ocv U ocv U x
32 10 31 mpbird φ x C x ran I
33 simpr φ x ran I x ran I
34 5 adantr φ x ran I K HL W H
35 1 13 2 14 dihrnss K HL W H x ran I x Base DVecH K W
36 5 35 sylan φ x ran I x Base DVecH K W
37 1 13 3 34 14 15 7 36 hlhilocv φ x ran I ocv U x = ocH K W x
38 37 fveq2d φ x ran I ocv U ocv U x = ocv U ocH K W x
39 34 36 24 syl2anc φ x ran I ocH K W x Base DVecH K W
40 1 13 3 34 14 15 7 39 hlhilocv φ x ran I ocv U ocH K W x = ocH K W ocH K W x
41 38 40 eqtrd φ x ran I ocv U ocv U x = ocH K W ocH K W x
42 41 eqeq1d φ x ran I ocv U ocv U x = x ocH K W ocH K W x = x
43 42 biimpar φ x ran I ocH K W ocH K W x = x ocv U ocv U x = x
44 43 eqcomd φ x ran I ocH K W ocH K W x = x x = ocv U ocv U x
45 44 ex φ x 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 φ x ran I x ran I ocH K W ocH K W x = x
47 6 8 mp1i φ x ran I x C x = ocv U ocv U x
48 45 46 47 3imtr4d φ x ran I x ran I x C
49 33 48 mpd φ x ran I x C
50 32 49 impbida φ x C x ran I
51 50 eqrdv φ C = ran I