Theorem dvhfmulr

Description: Ring multiplication operation for the constructed full vector space H. (Contributed by NM, 29-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

	Ref	Expression
Hypotheses	dvhfmul.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dvhfmul.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dvhfmul.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	dvhfmul.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dvhfmul.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
	dvhfmul.m	$$⊢\underset{\dot{}}{·}={\cdot }_F$$
Assertion	dvhfmulr	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{·}=\left(s\in E,t\in E⟼s\circ t\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvhfmul.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dvhfmul.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		dvhfmul.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
4		dvhfmul.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		dvhfmul.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
6		dvhfmul.m	$$⊢\underset{\dot{}}{·}={\cdot }_F$$
7		eqid	$$⊢\mathrm{EDRing}\left(K\right)\left(W\right)=\mathrm{EDRing}\left(K\right)\left(W\right)$$
8	1 7 4 5	dvhsca	$$⊢\left(K\in V\wedge W\in H\right)\to F=\mathrm{EDRing}\left(K\right)\left(W\right)$$
9	8	fveq2d	$$⊢\left(K\in V\wedge W\in H\right)\to {\cdot }_F={\cdot }_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
10	6 9	syl5eq	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{·}={\cdot }_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
11		eqid	$$⊢{\cdot }_{\mathrm{EDRing}\left(K\right)\left(W\right)}={\cdot }_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
12	1 2 3 7 11	erngfmul	$$⊢\left(K\in V\wedge W\in H\right)\to {\cdot }_{\mathrm{EDRing}\left(K\right)\left(W\right)}=\left(s\in E,t\in E⟼s\circ t\right)$$
13	10 12	eqtrd	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{·}=\left(s\in E,t\in E⟼s\circ t\right)$$