Theorem mendmulr

Description: A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015)

	Ref	Expression
Hypotheses	mendmulrfval.a	$$⊢A=\mathrm{MEndo}\left(M\right)$$
	mendmulrfval.b	$$⊢B={\mathrm{Base}}_A$$
	mendmulr.q	$$⊢\underset{\dot{}}{·}={\cdot }_A$$
Assertion	mendmulr	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}Y=X\circ Y$$

Proof

Step	Hyp	Ref	Expression
1		mendmulrfval.a	$$⊢A=\mathrm{MEndo}\left(M\right)$$
2		mendmulrfval.b	$$⊢B={\mathrm{Base}}_A$$
3		mendmulr.q	$$⊢\underset{\dot{}}{·}={\cdot }_A$$
4		coexg	$$⊢\left(X\in B\wedge Y\in B\right)\to X\circ Y\in \mathrm{V}$$
5		coeq1	$$⊢x=X\to x\circ y=X\circ y$$
6		coeq2	$$⊢y=Y\to X\circ y=X\circ Y$$
7	1 2	mendmulrfval	$$⊢{\cdot }_A=\left(x\in B,y\in B⟼x\circ y\right)$$
8	3 7	eqtri	$$⊢\underset{\dot{}}{·}=\left(x\in B,y\in B⟼x\circ y\right)$$
9	5 6 8	ovmpog	$$⊢\left(X\in B\wedge Y\in B\wedge X\circ Y\in \mathrm{V}\right)\to X\underset{\dot{}}{·}Y=X\circ Y$$
10	4 9	mpd3an3	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}Y=X\circ Y$$