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=\mathrm{LHyp}\left(K\right)$$
	hlhilslem.e	$$⊢E=\mathrm{EDRing}\left(K\right)\left(W\right)$$
	hlhilslem.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
	hlhilslem.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hlhilslem.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hlhilsmul.m	$$⊢\underset{\dot{}}{·}={\cdot }_E$$
Assertion	hlhilsmul	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_R$$

Proof

Step	Hyp	Ref	Expression
1		hlhilslem.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hlhilslem.e	$$⊢E=\mathrm{EDRing}\left(K\right)\left(W\right)$$
3		hlhilslem.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
4		hlhilslem.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
5		hlhilslem.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
6		hlhilsmul.m	$$⊢\underset{\dot{}}{·}={\cdot }_E$$
7		mulridx	$$⊢{\cdot }_{𝑟}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$
8		starvndxnmulrndx	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
9	8	necomi	$$⊢{\cdot }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
10	1 2 3 4 5 7 9 6	hlhilslem	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_R$$