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 = ( MEndo ` M )
	mendvscafval.v	|- .x. = ( .s ` M )
	mendvscafval.b	|- B = ( Base ` A )
	mendvscafval.s	|- S = ( Scalar ` M )
	mendvscafval.k	|- K = ( Base ` S )
	mendvscafval.e	|- E = ( Base ` M )
	mendvsca.w	|- .xb = ( .s ` A )
Assertion	mendvsca	|- ( ( X e. K /\ Y e. B ) -> ( X .xb Y ) = ( ( E X. { X } ) oF .x. Y ) )

Proof

Step	Hyp	Ref	Expression
1		mendvscafval.a	|- A = ( MEndo ` M )
2		mendvscafval.v	|- .x. = ( .s ` M )
3		mendvscafval.b	|- B = ( Base ` A )
4		mendvscafval.s	|- S = ( Scalar ` M )
5		mendvscafval.k	|- K = ( Base ` S )
6		mendvscafval.e	|- E = ( Base ` M )
7		mendvsca.w	|- .xb = ( .s ` A )
8		sneq	|- ( x = X -> { x } = { X } )
9	8	xpeq2d	|- ( x = X -> ( E X. { x } ) = ( E X. { X } ) )
10		id	|- ( y = Y -> y = Y )
11	9 10	oveqan12d	|- ( ( x = X /\ y = Y ) -> ( ( E X. { x } ) oF .x. y ) = ( ( E X. { X } ) oF .x. Y ) )
12	1 2 3 4 5 6	mendvscafval	|- ( .s ` A ) = ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) )
13	7 12	eqtri	|- .xb = ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) )
14		ovex	|- ( ( E X. { X } ) oF .x. Y ) e. _V
15	11 13 14	ovmpoa	|- ( ( X e. K /\ Y e. B ) -> ( X .xb Y ) = ( ( E X. { X } ) oF .x. Y ) )