Theorem mavmumamul1

Description: The multiplication of an NxN matrix with an N-dimensional vector corresponds to the matrix multiplication of an NxN matrix with an Nx1 matrix. (Contributed by AV, 14-Mar-2019)

	Ref	Expression
Hypotheses	mavmumamul1.a	|- A = ( N Mat R )
	mavmumamul1.m	|- .X. = ( R maMul <. N , N , { (/) } >. )
	mavmumamul1.t	|- .x. = ( R maVecMul <. N , N >. )
	mavmumamul1.b	|- B = ( Base ` R )
	mavmumamul1.r	|- ( ph -> R e. Ring )
	mavmumamul1.n	|- ( ph -> N e. Fin )
	mavmumamul1.x	|- ( ph -> X e. ( Base ` A ) )
	mavmumamul1.y	|- ( ph -> Y e. ( B ^m N ) )
	mavmumamul1.z	|- ( ph -> Z e. ( B ^m ( N X. { (/) } ) ) )
Assertion	mavmumamul1	|- ( ph -> ( A. j e. N ( Y ` j ) = ( j Z (/) ) -> A. i e. N ( ( X .x. Y ) ` i ) = ( i ( X .X. Z ) (/) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mavmumamul1.a	|- A = ( N Mat R )
2		mavmumamul1.m	|- .X. = ( R maMul <. N , N , { (/) } >. )
3		mavmumamul1.t	|- .x. = ( R maVecMul <. N , N >. )
4		mavmumamul1.b	|- B = ( Base ` R )
5		mavmumamul1.r	|- ( ph -> R e. Ring )
6		mavmumamul1.n	|- ( ph -> N e. Fin )
7		mavmumamul1.x	|- ( ph -> X e. ( Base ` A ) )
8		mavmumamul1.y	|- ( ph -> Y e. ( B ^m N ) )
9		mavmumamul1.z	|- ( ph -> Z e. ( B ^m ( N X. { (/) } ) ) )
10	1 4	matbas2	|- ( ( N e. Fin /\ R e. Ring ) -> ( B ^m ( N X. N ) ) = ( Base ` A ) )
11	6 5 10	syl2anc	|- ( ph -> ( B ^m ( N X. N ) ) = ( Base ` A ) )
12	7 11	eleqtrrd	|- ( ph -> X e. ( B ^m ( N X. N ) ) )
13	2 3 4 5 6 6 12 8 9	mvmumamul1	|- ( ph -> ( A. j e. N ( Y ` j ) = ( j Z (/) ) -> A. i e. N ( ( X .x. Y ) ` i ) = ( i ( X .X. Z ) (/) ) ) )