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 bitrid ⊢ φ ∧ 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