Metamath Proof Explorer


Theorem hlhilsmul2

Description: Scalar multiplication for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

Ref Expression
Hypotheses hlhilsbase.h
|- H = ( LHyp ` K )
hlhilsbase.l
|- L = ( ( DVecH ` K ) ` W )
hlhilsbase.s
|- S = ( Scalar ` L )
hlhilsbase.u
|- U = ( ( HLHil ` K ) ` W )
hlhilsbase.r
|- R = ( Scalar ` U )
hlhilsbase.k
|- ( ph -> ( K e. HL /\ W e. H ) )
hlhilsmul2.m
|- .x. = ( .r ` S )
Assertion hlhilsmul2
|- ( ph -> .x. = ( .r ` R ) )

Proof

Step Hyp Ref Expression
1 hlhilsbase.h
 |-  H = ( LHyp ` K )
2 hlhilsbase.l
 |-  L = ( ( DVecH ` K ) ` W )
3 hlhilsbase.s
 |-  S = ( Scalar ` L )
4 hlhilsbase.u
 |-  U = ( ( HLHil ` K ) ` W )
5 hlhilsbase.r
 |-  R = ( Scalar ` U )
6 hlhilsbase.k
 |-  ( ph -> ( K e. HL /\ W e. H ) )
7 hlhilsmul2.m
 |-  .x. = ( .r ` S )
8 eqid
 |-  ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W )
9 1 8 2 3 dvhsca
 |-  ( ( K e. HL /\ W e. H ) -> S = ( ( EDRing ` K ) ` W ) )
10 6 9 syl
 |-  ( ph -> S = ( ( EDRing ` K ) ` W ) )
11 10 fveq2d
 |-  ( ph -> ( .r ` S ) = ( .r ` ( ( EDRing ` K ) ` W ) ) )
12 7 11 syl5eq
 |-  ( ph -> .x. = ( .r ` ( ( EDRing ` K ) ` W ) ) )
13 eqid
 |-  ( .r ` ( ( EDRing ` K ) ` W ) ) = ( .r ` ( ( EDRing ` K ) ` W ) )
14 1 8 4 5 6 13 hlhilsmul
 |-  ( ph -> ( .r ` ( ( EDRing ` K ) ` W ) ) = ( .r ` R ) )
15 12 14 eqtrd
 |-  ( ph -> .x. = ( .r ` R ) )