Description: Construction of a Hilbert space ( df-hil ) U from a Hilbert lattice ( df-hlat ) K , where W is a fixed but arbitrary hyperplane (co-atom) in K .
The Hilbert space U is identical to the vector space ( ( DVecHK )W ) (see dvhlvec ) except that it is extended with involution and inner product components. The construction of these two components is provided by Theorem 3.6 in Holland95 p. 13, whose proof we follow loosely.
An example of involution is the complex conjugate when the division ring is the field of complex numbers. The nature of the division ring we constructed is indeterminate, however, until we specialize the initial Hilbert lattice with additional conditions found by Maria Solèr in 1995 and refined by René Mayet in 1998 that result in a division ring isomorphic to CC . See additional discussion at https://us.metamath.org/qlegif/mmql.html#what .
W corresponds to the w in the proof of Theorem 13.4 of Crawley p. 111. Such a W always exists since HL has lattice rank of at least 4 by df-hil . It can be eliminated if we just want to show the existence of a Hilbert space, as is done in the literature. (Contributed by NM, 23-Jun-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hlhilphl.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
| hlhilphllem.u | ⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 ) | ||
| hlhilphl.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | ||
| Assertion | hlathil | ⊢ ( 𝜑 → 𝑈 ∈ Hil ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hlhilphl.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
| 2 | hlhilphllem.u | ⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 ) | |
| 3 | hlhilphl.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | |
| 4 | eqid | ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 ) | |
| 5 | eqid | ⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) | |
| 6 | eqid | ⊢ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) | |
| 7 | eqid | ⊢ ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) | |
| 8 | eqid | ⊢ ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) | |
| 9 | eqid | ⊢ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) | |
| 10 | eqid | ⊢ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) | |
| 11 | eqid | ⊢ ( +g ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( +g ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) | |
| 12 | eqid | ⊢ ( .r ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( .r ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) | |
| 13 | eqid | ⊢ ( 0g ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) | |
| 14 | eqid | ⊢ ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) | |
| 15 | eqid | ⊢ ( ·𝑖 ‘ 𝑈 ) = ( ·𝑖 ‘ 𝑈 ) | |
| 16 | eqid | ⊢ ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) | |
| 17 | eqid | ⊢ ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) | |
| 18 | eqid | ⊢ ( 𝑥 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) , 𝑦 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ↦ ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑦 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) , 𝑦 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ↦ ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑦 ) ‘ 𝑥 ) ) | |
| 19 | eqid | ⊢ ( ocv ‘ 𝑈 ) = ( ocv ‘ 𝑈 ) | |
| 20 | eqid | ⊢ ( ClSubSp ‘ 𝑈 ) = ( ClSubSp ‘ 𝑈 ) | |
| 21 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 | hlhilhillem | ⊢ ( 𝜑 → 𝑈 ∈ Hil ) |