Theorem mavmulfv

Description: A cell/element in the vector resulting from a multiplication of a vector with a square matrix. (Contributed by AV, 6-Dec-2018) (Revised by AV, 18-Feb-2019) (Revised by AV, 23-Feb-2019)

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

Proof

Step	Hyp	Ref	Expression
1		mavmulval.a	|- A = ( N Mat R )
2		mavmulval.m	|- .X. = ( R maVecMul <. N , N >. )
3		mavmulval.b	|- B = ( Base ` R )
4		mavmulval.t	|- .x. = ( .r ` R )
5		mavmulval.r	|- ( ph -> R e. V )
6		mavmulval.n	|- ( ph -> N e. Fin )
7		mavmulval.x	|- ( ph -> X e. ( Base ` A ) )
8		mavmulval.y	|- ( ph -> Y e. ( B ^m N ) )
9		mavmulfv.i	|- ( ph -> I e. N )
10	1 2 3 4 5 6 7 8	mavmulval	|- ( ph -> ( X .X. Y ) = ( i e. N |-> ( 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 ) ) ) ) )