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 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion hlhillvec 
|- ( ph -> U e. LVec )

Proof

Step Hyp Ref Expression
1 hlhillvec.h 
 |-  H = ( LHyp ` K )
2 hlhillvec.u 
 |-  U = ( ( HLHil ` K ) ` W )
3 hlhillvec.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
4 eqid 
 |-  ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
5 1 4 3 dvhlvec 
 |-  ( ph -> ( ( DVecH ` K ) ` W ) e. LVec )
6 eqidd 
 |-  ( ph -> ( 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 
 |-  ( ph -> ( Base ` ( ( DVecH ` K ) ` W ) ) = ( Base ` U ) )
9 eqid 
 |-  ( Scalar ` ( ( DVecH ` K ) ` W ) ) = ( Scalar ` ( ( DVecH ` K ) ` W ) )
10 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
11 eqidd 
 |-  ( ph -> ( 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 
 |-  ( ph -> ( Base ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) ) = ( Base ` ( Scalar ` U ) ) )
14 eqid 
 |-  ( +g ` ( ( DVecH ` K ) ` W ) ) = ( +g ` ( ( DVecH ` K ) ` W ) )
15 1 2 3 4 14 hlhilplus 
 |-  ( ph -> ( +g ` ( ( DVecH ` K ) ` W ) ) = ( +g ` U ) )
16 15 oveqdr 
 |-  ( ( ph /\ ( x e. ( Base ` ( ( DVecH ` K ) ` W ) ) /\ y e. ( Base ` ( ( DVecH ` K ) ` W ) ) ) ) -> ( x ( +g ` ( ( DVecH ` K ) ` W ) ) y ) = ( x ( +g ` U ) y ) )
17 eqid 
 |-  ( +g ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) ) = ( +g ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) )
18 1 4 9 2 10 3 17 hlhilsplus2 
 |-  ( ph -> ( +g ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) ) = ( +g ` ( Scalar ` U ) ) )
19 18 oveqdr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) ) /\ y e. ( Base ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) ) ) ) -> ( x ( +g ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) ) y ) = ( x ( +g ` ( Scalar ` U ) ) y ) )
20 eqid 
 |-  ( .r ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) ) = ( .r ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) )
21 1 4 9 2 10 3 20 hlhilsmul2 
 |-  ( ph -> ( .r ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) ) = ( .r ` ( Scalar ` U ) ) )
22 21 oveqdr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) ) /\ y e. ( Base ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) ) ) ) -> ( x ( .r ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) ) y ) = ( x ( .r ` ( Scalar ` U ) ) y ) )
23 eqid 
 |-  ( .s ` ( ( DVecH ` K ) ` W ) ) = ( .s ` ( ( DVecH ` K ) ` W ) )
24 1 4 23 2 3 hlhilvsca 
 |-  ( ph -> ( .s ` ( ( DVecH ` K ) ` W ) ) = ( .s ` U ) )
25 24 oveqdr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` ( ( DVecH ` K ) ` W ) ) ) /\ y e. ( Base ` ( ( DVecH ` K ) ` W ) ) ) ) -> ( x ( .s ` ( ( DVecH ` K ) ` W ) ) y ) = ( x ( .s ` U ) y ) )
26 6 8 9 10 11 13 16 19 22 25 lvecprop2d 
 |-  ( ph -> ( ( ( DVecH ` K ) ` W ) e. LVec <-> U e. LVec ) )
27 5 26 mpbid 
 |-  ( ph -> U e. LVec )