Theorem mendvsca

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

	Ref	Expression
Hypotheses	mendvscafval.a	$$⊢A=\mathrm{MEndo}\left(M\right)$$
	mendvscafval.v	$$⊢\underset{\dot{}}{·}={\cdot }_M$$
	mendvscafval.b	$$⊢B={\mathrm{Base}}_A$$
	mendvscafval.s	$$⊢S=\mathrm{Scalar}\left(M\right)$$
	mendvscafval.k	$$⊢K={\mathrm{Base}}_S$$
	mendvscafval.e	$$⊢E={\mathrm{Base}}_M$$
	mendvsca.w	$$⊢\underset{\dot{}}{\bullet }={\cdot }_A$$
Assertion	mendvsca	$$⊢\left(X\in K\wedge Y\in B\right)\to X\underset{\dot{}}{\bullet }Y=\left(E\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y$$

Proof

Step	Hyp	Ref	Expression
1		mendvscafval.a	$$⊢A=\mathrm{MEndo}\left(M\right)$$
2		mendvscafval.v	$$⊢\underset{\dot{}}{·}={\cdot }_M$$
3		mendvscafval.b	$$⊢B={\mathrm{Base}}_A$$
4		mendvscafval.s	$$⊢S=\mathrm{Scalar}\left(M\right)$$
5		mendvscafval.k	$$⊢K={\mathrm{Base}}_S$$
6		mendvscafval.e	$$⊢E={\mathrm{Base}}_M$$
7		mendvsca.w	$$⊢\underset{\dot{}}{\bullet }={\cdot }_A$$
8		sneq	$$⊢x=X\to \left\{x\right\}=\left\{X\right\}$$
9	8	xpeq2d	$$⊢x=X\to E\times \left\{x\right\}=E\times \left\{X\right\}$$
10		id	$$⊢y=Y\to y=Y$$
11	9 10	oveqan12d	$$⊢\left(x=X\wedge y=Y\right)\to \left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y=\left(E\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y$$
12	1 2 3 4 5 6	mendvscafval	$$⊢{\cdot }_A=\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)$$
13	7 12	eqtri	$$⊢\underset{\dot{}}{\bullet }=\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)$$
14		ovex	$$⊢\left(E\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\in \mathrm{V}$$
15	11 13 14	ovmpoa	$$⊢\left(X\in K\wedge Y\in B\right)\to X\underset{\dot{}}{\bullet }Y=\left(E\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y$$