Theorem mvmulfv

Description: A cell/element in the vector resulting from a 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 ) )
	mvmulfv.i	|- ( ph -> I e. M )
Assertion	mvmulfv	|- ( ph -> ( ( X .X. Y ) ` I ) = ( 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		mvmulfv.i	|- ( ph -> I e. M )
10	1 2 3 4 5 6 7 8	mvmulval	|- ( ph -> ( X .X. Y ) = ( i e. M |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) )
11		oveq1	|- ( i = I -> ( i X j ) = ( I X j ) )
12	11	adantl	|- ( ( ph /\ i = I ) -> ( i X j ) = ( I X j ) )
13	12	oveq1d	|- ( ( ph /\ i = I ) -> ( ( i X j ) .x. ( Y ` j ) ) = ( ( I X j ) .x. ( Y ` j ) ) )
14	13	mpteq2dv	|- ( ( ph /\ i = I ) -> ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) = ( j e. N |-> ( ( I X j ) .x. ( Y ` j ) ) ) )
15	14	oveq2d	|- ( ( ph /\ i = I ) -> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) = ( R gsum ( j e. N |-> ( ( I X j ) .x. ( Y ` j ) ) ) ) )
16		ovexd	|- ( ph -> ( R gsum ( j e. N |-> ( ( I X j ) .x. ( Y ` j ) ) ) ) e. _V )
17	10 15 9 16	fvmptd	|- ( ph -> ( ( X .X. Y ) ` I ) = ( R gsum ( j e. N |-> ( ( I X j ) .x. ( Y ` j ) ) ) ) )