Theorem hlhilsmul2

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	hlhilsbase.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hlhilsbase.l	$$⊢L=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hlhilsbase.s	$$⊢S=\mathrm{Scalar}\left(L\right)$$
	hlhilsbase.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
	hlhilsbase.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hlhilsbase.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hlhilsmul2.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
Assertion	hlhilsmul2	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_R$$

Proof

Step	Hyp	Ref	Expression
1		hlhilsbase.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hlhilsbase.l	$$⊢L=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hlhilsbase.s	$$⊢S=\mathrm{Scalar}\left(L\right)$$
4		hlhilsbase.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
5		hlhilsbase.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
6		hlhilsbase.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7		hlhilsmul2.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
8		eqid	$$⊢\mathrm{EDRing}\left(K\right)\left(W\right)=\mathrm{EDRing}\left(K\right)\left(W\right)$$
9	1 8 2 3	dvhsca	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to S=\mathrm{EDRing}\left(K\right)\left(W\right)$$
10	6 9	syl	$$⊢\phi \to S=\mathrm{EDRing}\left(K\right)\left(W\right)$$
11	10	fveq2d	$$⊢\phi \to {\cdot }_S={\cdot }_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
12	7 11	syl5eq	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
13		eqid	$$⊢{\cdot }_{\mathrm{EDRing}\left(K\right)\left(W\right)}={\cdot }_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
14	1 8 4 5 6 13	hlhilsmul	$$⊢\phi \to {\cdot }_{\mathrm{EDRing}\left(K\right)\left(W\right)}={\cdot }_R$$
15	12 14	eqtrd	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_R$$