Metamath Proof Explorer


Theorem hlhilsmul

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

Ref Expression
Hypotheses hlhilslem.h
|- H = ( LHyp ` K )
hlhilslem.e
|- E = ( ( EDRing ` K ) ` W )
hlhilslem.u
|- U = ( ( HLHil ` K ) ` W )
hlhilslem.r
|- R = ( Scalar ` U )
hlhilslem.k
|- ( ph -> ( K e. HL /\ W e. H ) )
hlhilsmul.m
|- .x. = ( .r ` E )
Assertion hlhilsmul
|- ( ph -> .x. = ( .r ` R ) )

Proof

Step Hyp Ref Expression
1 hlhilslem.h
 |-  H = ( LHyp ` K )
2 hlhilslem.e
 |-  E = ( ( EDRing ` K ) ` W )
3 hlhilslem.u
 |-  U = ( ( HLHil ` K ) ` W )
4 hlhilslem.r
 |-  R = ( Scalar ` U )
5 hlhilslem.k
 |-  ( ph -> ( K e. HL /\ W e. H ) )
6 hlhilsmul.m
 |-  .x. = ( .r ` E )
7 mulrid
 |-  .r = Slot ( .r ` ndx )
8 starvndxnmulrndx
 |-  ( *r ` ndx ) =/= ( .r ` ndx )
9 8 necomi
 |-  ( .r ` ndx ) =/= ( *r ` ndx )
10 1 2 3 4 5 7 9 6 hlhilslem
 |-  ( ph -> .x. = ( .r ` R ) )