Metamath Proof Explorer


Theorem hlhillvec

Description: The final constructed Hilbert space is a vector space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 29-Jun-2015)

Ref Expression
Hypotheses hlhillvec.h H = LHyp K
hlhillvec.u U = HLHil K W
hlhillvec.k φ K HL W H
Assertion hlhillvec φ U LVec

Proof

Step Hyp Ref Expression
1 hlhillvec.h H = LHyp K
2 hlhillvec.u U = HLHil K W
3 hlhillvec.k φ K HL W H
4 eqid DVecH K W = DVecH K W
5 1 4 3 dvhlvec φ DVecH K W LVec
6 eqidd φ Base DVecH K W = Base DVecH K W
7 eqid Base DVecH K W = Base DVecH K W
8 1 2 3 4 7 hlhilbase φ Base DVecH K W = Base U
9 eqid Scalar DVecH K W = Scalar DVecH K W
10 eqid Scalar U = Scalar U
11 eqidd φ Base Scalar DVecH K W = Base Scalar DVecH K W
12 eqid Base Scalar DVecH K W = Base Scalar DVecH K W
13 1 4 9 2 10 3 12 hlhilsbase2 φ Base Scalar DVecH K W = Base Scalar U
14 eqid + DVecH K W = + DVecH K W
15 1 2 3 4 14 hlhilplus φ + DVecH K W = + U
16 15 oveqdr φ x Base DVecH K W y Base DVecH K W x + DVecH K W y = x + U y
17 eqid + Scalar DVecH K W = + Scalar DVecH K W
18 1 4 9 2 10 3 17 hlhilsplus2 φ + Scalar DVecH K W = + Scalar U
19 18 oveqdr φ x Base Scalar DVecH K W y Base Scalar DVecH K W x + Scalar DVecH K W y = x + Scalar U y
20 eqid Scalar DVecH K W = Scalar DVecH K W
21 1 4 9 2 10 3 20 hlhilsmul2 φ Scalar DVecH K W = Scalar U
22 21 oveqdr φ x Base Scalar DVecH K W y Base Scalar DVecH K W x Scalar DVecH K W y = x Scalar U y
23 eqid DVecH K W = DVecH K W
24 1 4 23 2 3 hlhilvsca φ DVecH K W = U
25 24 oveqdr φ x Base Scalar DVecH K W y Base DVecH K W x DVecH K W y = x U y
26 6 8 9 10 11 13 16 19 22 25 lvecprop2d φ DVecH K W LVec U LVec
27 5 26 mpbid φ U LVec