Theorem dvafmulr

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

	Ref	Expression
Hypotheses	dvafmul.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dvafmul.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dvafmul.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	dvafmul.u	$$⊢U=\mathrm{DVecA}\left(K\right)\left(W\right)$$
	dvafmul.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
	dvafmul.p	$$⊢\underset{\dot{}}{·}={\cdot }_F$$
Assertion	dvafmulr	$$⊢\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		dvafmul.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dvafmul.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		dvafmul.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
4		dvafmul.u	$$⊢U=\mathrm{DVecA}\left(K\right)\left(W\right)$$
5		dvafmul.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
6		dvafmul.p	$$⊢\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	dvasca	$$⊢\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)$$