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 𝐻 = ( LHyp ‘ 𝐾 )
hlhilslem.e 𝐸 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
hlhilslem.u 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
hlhilslem.r 𝑅 = ( Scalar ‘ 𝑈 )
hlhilslem.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hlhilsmul.m · = ( .r𝐸 )
Assertion hlhilsmul ( 𝜑· = ( .r𝑅 ) )

Proof

Step Hyp Ref Expression
1 hlhilslem.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hlhilslem.e 𝐸 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
3 hlhilslem.u 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
4 hlhilslem.r 𝑅 = ( Scalar ‘ 𝑈 )
5 hlhilslem.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
6 hlhilsmul.m · = ( .r𝐸 )
7 mulrid .r = Slot ( .r ‘ ndx )
8 starvndxnmulrndx ( *𝑟 ‘ ndx ) ≠ ( .r ‘ ndx )
9 8 necomi ( .r ‘ ndx ) ≠ ( *𝑟 ‘ ndx )
10 1 2 3 4 5 7 9 6 hlhilslem ( 𝜑· = ( .r𝑅 ) )