Theorem mvmulval

Description: Multiplication of a vector with a matrix. (Contributed by AV, 23-Feb-2019)

	Ref	Expression
Hypotheses	mvmulfval.x	|- .X. = ( R maVecMul <. M , N >. )
	mvmulfval.b	|- B = ( Base ` R )
	mvmulfval.t	|- .x. = ( .r ` R )
	mvmulfval.r	|- ( ph -> R e. V )
	mvmulfval.m	|- ( ph -> M e. Fin )
	mvmulfval.n	|- ( ph -> N e. Fin )
	mvmulval.x	|- ( ph -> X e. ( B ^m ( M X. N ) ) )
	mvmulval.y	|- ( ph -> Y e. ( B ^m N ) )
Assertion	mvmulval	|- ( ph -> ( X .X. Y ) = ( i e. M |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mvmulfval.x	|- .X. = ( R maVecMul <. M , N >. )
2		mvmulfval.b	|- B = ( Base ` R )
3		mvmulfval.t	|- .x. = ( .r ` R )
4		mvmulfval.r	|- ( ph -> R e. V )
5		mvmulfval.m	|- ( ph -> M e. Fin )
6		mvmulfval.n	|- ( ph -> N e. Fin )
7		mvmulval.x	|- ( ph -> X e. ( B ^m ( M X. N ) ) )
8		mvmulval.y	|- ( ph -> Y e. ( B ^m N ) )
9	1 2 3 4 5 6	mvmulfval	|- ( ph -> .X. = ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m N ) |-> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( y ` j ) ) ) ) ) ) )
10		oveq	|- ( x = X -> ( i x j ) = ( i X j ) )
11		fveq1	|- ( y = Y -> ( y ` j ) = ( Y ` j ) )
12	10 11	oveqan12d	|- ( ( x = X /\ y = Y ) -> ( ( i x j ) .x. ( y ` j ) ) = ( ( i X j ) .x. ( Y ` j ) ) )
13	12	adantl	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( i x j ) .x. ( y ` j ) ) = ( ( i X j ) .x. ( Y ` j ) ) )
14	13	mpteq2dv	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( j e. N |-> ( ( i x j ) .x. ( y ` j ) ) ) = ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) )
15	14	oveq2d	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( y ` j ) ) ) ) = ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) )
16	15	mpteq2dv	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( y ` j ) ) ) ) ) = ( i e. M |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) )
17	5	mptexd	|- ( ph -> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) e. _V )
18	9 16 7 8 17	ovmpod	|- ( ph -> ( X .X. Y ) = ( i e. M |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) )