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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hlhillcs.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
hlhillcs.u ⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
hlhillcs.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑈 )
hlhillcs.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion hlhillcs ( 𝜑 → 𝐶 = ran 𝐼 )

Proof

Step Hyp Ref Expression
1 hlhillcs.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hlhillcs.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 hlhillcs.u ⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
4 hlhillcs.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑈 )
5 hlhillcs.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 3 fvexi ⊢ 𝑈 ∈ V
7 eqid ⊢ ( ocv ‘ 𝑈 ) = ( ocv ‘ 𝑈 )
8 7 4 iscss ⊢ ( 𝑈 ∈ V → ( 𝑥 ∈ 𝐶 ↔ 𝑥 = ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) ) )
9 6 8 mp1i ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↔ 𝑥 = ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) ) )
10 9 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 = ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) )
11 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
12 11 4 cssss ⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ⊆ ( Base ‘ 𝑈 ) )
13 eqid ⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
14 eqid ⊢ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
15 eqid ⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
16 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( Base ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17 1 3 5 13 14 hlhilbase ⊢ ( 𝜑 → ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ 𝑈 ) )
18 17 sseq2d ⊢ ( 𝜑 → ( 𝑥 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ 𝑥 ⊆ ( Base ‘ 𝑈 ) ) )
19 18 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( Base ‘ 𝑈 ) ) → 𝑥 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
20 1 2 13 14 15 16 19 dochoccl ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( Base ‘ 𝑈 ) ) → ( 𝑥 ∈ ran 𝐼 ↔ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = 𝑥 ) )
21 eqcom ⊢ ( 𝑥 = ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) ↔ ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) = 𝑥 )
22 1 13 3 16 14 15 7 19 hlhilocv ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( Base ‘ 𝑈 ) ) → ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) )
23 22 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( Base ‘ 𝑈 ) ) → ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) = ( ( ocv ‘ 𝑈 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) )
24 1 13 14 15 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
25 16 19 24 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( Base ‘ 𝑈 ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
26 1 13 3 16 14 15 7 25 hlhilocv ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( Base ‘ 𝑈 ) ) → ( ( ocv ‘ 𝑈 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) )
27 23 26 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( Base ‘ 𝑈 ) ) → ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) )
28 27 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( Base ‘ 𝑈 ) ) → ( ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) = 𝑥 ↔ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = 𝑥 ) )
29 21 28 syl5bb ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( Base ‘ 𝑈 ) ) → ( 𝑥 = ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) ↔ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = 𝑥 ) )
30 20 29 bitr4d ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( Base ‘ 𝑈 ) ) → ( 𝑥 ∈ ran 𝐼 ↔ 𝑥 = ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) ) )
31 12 30 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ ran 𝐼 ↔ 𝑥 = ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) ) )
32 10 31 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ran 𝐼 )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) → 𝑥 ∈ ran 𝐼 )
34 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
35 1 13 2 14 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ran 𝐼 ) → 𝑥 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
36 5 35 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) → 𝑥 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
37 1 13 3 34 14 15 7 36 hlhilocv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) → ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) )
38 37 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) → ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) = ( ( ocv ‘ 𝑈 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) )
39 34 36 24 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
40 1 13 3 34 14 15 7 39 hlhilocv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) → ( ( ocv ‘ 𝑈 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) )
41 38 40 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) → ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) )
42 41 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) → ( ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) = 𝑥 ↔ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = 𝑥 ) )
43 42 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = 𝑥 ) → ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) = 𝑥 )
44 43 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = 𝑥 ) → 𝑥 = ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) )
45 44 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) → ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = 𝑥 → 𝑥 = ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) ) )
46 1 2 13 14 15 34 36 dochoccl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) → ( 𝑥 ∈ ran 𝐼 ↔ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = 𝑥 ) )
47 6 8 mp1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) → ( 𝑥 ∈ 𝐶 ↔ 𝑥 = ( ( ocv ‘ 𝑈 ) ‘ ( ( ocv ‘ 𝑈 ) ‘ 𝑥 ) ) ) )
48 45 46 47 3imtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) → ( 𝑥 ∈ ran 𝐼 → 𝑥 ∈ 𝐶 ) )
49 33 48 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐼 ) → 𝑥 ∈ 𝐶 )
50 32 49 impbida ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ran 𝐼 ) )
51 50 eqrdv ⊢ ( 𝜑 → 𝐶 = ran 𝐼 )