Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of involution and inner product from a Hilbert lattice
hlhilsmul
Metamath Proof Explorer
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 ‘ 𝑅 ) )