Theorem mavmulval

Description: Multiplication of a vector with a square matrix. (Contributed 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 ) )
Assertion	mavmulval	|- ( ph -> ( X .X. Y ) = ( i e. N |-> ( 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	1 3	matbas2	|- ( ( N e. Fin /\ R e. V ) -> ( B ^m ( N X. N ) ) = ( Base ` A ) )
10	6 5 9	syl2anc	|- ( ph -> ( B ^m ( N X. N ) ) = ( Base ` A ) )
11	7 10	eleqtrrd	|- ( ph -> X e. ( B ^m ( N X. N ) ) )
12	2 3 4 5 6 6 11 8	mvmulval	|- ( ph -> ( X .X. Y ) = ( i e. N |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) )