Theorem hlhilsmul

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	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		df-mulr	|- .r = Slot 3
8		3nn	|- 3 e. NN
9		3lt4	|- 3 < 4
10	1 2 3 4 5 7 8 9 6	hlhilslem	|- ( ph -> .x. = ( .r ` R ) )