This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvhlvec

Description: The full vector space U constructed from a Hilbert lattice K (given a fiducial hyperplane W ) is a left module. (Contributed by NM, 23-May-2015)

Ref Expression
Hypotheses dvhlvec.h ⊢ H = LHyp ⁡ K
dvhlvec.u ⊢ U = DVecH ⁡ K ⁡ W
dvhlvec.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion dvhlvec ⊢ φ → U ∈ LVec

Proof

Step Hyp Ref Expression
1 dvhlvec.h ⊢ H = LHyp ⁡ K
2 dvhlvec.u ⊢ U = DVecH ⁡ K ⁡ W
3 dvhlvec.k ⊢ φ → K ∈ HL ∧ W ∈ H
4 eqid ⊢ Base K = Base K
5 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
6 eqid ⊢ TEndo ⁡ K ⁡ W = TEndo ⁡ K ⁡ W
7 eqid ⊢ Scalar ⁡ U = Scalar ⁡ U
8 eqid ⊢ + Scalar ⁡ U = + Scalar ⁡ U
9 eqid ⊢ + U = + U
10 eqid ⊢ 0 Scalar ⁡ U = 0 Scalar ⁡ U
11 eqid ⊢ inv g ⁡ Scalar ⁡ U = inv g ⁡ Scalar ⁡ U
12 eqid ⊢ ⋅ Scalar ⁡ U = ⋅ Scalar ⁡ U
13 eqid ⊢ ⋅ U = ⋅ U
14 4 1 5 6 2 7 8 9 10 11 12 13 dvhlveclem ⊢ K ∈ HL ∧ W ∈ H → U ∈ LVec
15 3 14 syl ⊢ φ → U ∈ LVec