Metamath Proof Explorer

Theorem mvmumamul1

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

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

Proof

Step Hyp Ref Expression
1 mvmumamul1.x 
 |-  .X. = ( R maMul <. M , N , { (/) } >. )
2 mvmumamul1.t 
 |-  .x. = ( R maVecMul <. M , N >. )
3 mvmumamul1.b 
 |-  B = ( Base ` R )
4 mvmumamul1.r 
 |-  ( ph -> R e. Ring )
5 mvmumamul1.m 
 |-  ( ph -> M e. Fin )
6 mvmumamul1.n 
 |-  ( ph -> N e. Fin )
7 mvmumamul1.a 
 |-  ( ph -> A e. ( B ^m ( M X. N ) ) )
8 mvmumamul1.y 
 |-  ( ph -> Y e. ( B ^m N ) )
9 mvmumamul1.z 
 |-  ( ph -> Z e. ( B ^m ( N X. { (/) } ) ) )
10 eqid 
 |-  ( .r ` R ) = ( .r ` R )
11 4 adantr 
 |-  ( ( ph /\ i e. M ) -> R e. Ring )
12 5 adantr 
 |-  ( ( ph /\ i e. M ) -> M e. Fin )
13 6 adantr 
 |-  ( ( ph /\ i e. M ) -> N e. Fin )
14 7 adantr 
 |-  ( ( ph /\ i e. M ) -> A e. ( B ^m ( M X. N ) ) )
15 8 adantr 
 |-  ( ( ph /\ i e. M ) -> Y e. ( B ^m N ) )
16 simpr 
 |-  ( ( ph /\ i e. M ) -> i e. M )
17 2 3 10 11 12 13 14 15 16 mvmulfv 
 |-  ( ( ph /\ i e. M ) -> ( ( A .x. Y ) ` i ) = ( R gsum ( k e. N |-> ( ( i A k ) ( .r ` R ) ( Y ` k ) ) ) ) )
18 17 adantlr 
 |-  ( ( ( ph /\ A. j e. N ( Y ` j ) = ( j Z (/) ) ) /\ i e. M ) -> ( ( A .x. Y ) ` i ) = ( R gsum ( k e. N |-> ( ( i A k ) ( .r ` R ) ( Y ` k ) ) ) ) )
19 fveq2 
 |-  ( j = k -> ( Y ` j ) = ( Y ` k ) )
20 oveq1 
 |-  ( j = k -> ( j Z (/) ) = ( k Z (/) ) )
21 19 20 eqeq12d 
 |-  ( j = k -> ( ( Y ` j ) = ( j Z (/) ) <-> ( Y ` k ) = ( k Z (/) ) ) )
22 21 rspccv 
 |-  ( A. j e. N ( Y ` j ) = ( j Z (/) ) -> ( k e. N -> ( Y ` k ) = ( k Z (/) ) ) )
23 22 adantl 
 |-  ( ( ph /\ A. j e. N ( Y ` j ) = ( j Z (/) ) ) -> ( k e. N -> ( Y ` k ) = ( k Z (/) ) ) )
24 23 imp 
 |-  ( ( ( ph /\ A. j e. N ( Y ` j ) = ( j Z (/) ) ) /\ k e. N ) -> ( Y ` k ) = ( k Z (/) ) )
25 24 oveq2d 
 |-  ( ( ( ph /\ A. j e. N ( Y ` j ) = ( j Z (/) ) ) /\ k e. N ) -> ( ( i A k ) ( .r ` R ) ( Y ` k ) ) = ( ( i A k ) ( .r ` R ) ( k Z (/) ) ) )
26 25 mpteq2dva 
 |-  ( ( ph /\ A. j e. N ( Y ` j ) = ( j Z (/) ) ) -> ( k e. N |-> ( ( i A k ) ( .r ` R ) ( Y ` k ) ) ) = ( k e. N |-> ( ( i A k ) ( .r ` R ) ( k Z (/) ) ) ) )
27 26 oveq2d 
 |-  ( ( ph /\ A. j e. N ( Y ` j ) = ( j Z (/) ) ) -> ( R gsum ( k e. N |-> ( ( i A k ) ( .r ` R ) ( Y ` k ) ) ) ) = ( R gsum ( k e. N |-> ( ( i A k ) ( .r ` R ) ( k Z (/) ) ) ) ) )
28 27 adantr 
 |-  ( ( ( ph /\ A. j e. N ( Y ` j ) = ( j Z (/) ) ) /\ i e. M ) -> ( R gsum ( k e. N |-> ( ( i A k ) ( .r ` R ) ( Y ` k ) ) ) ) = ( R gsum ( k e. N |-> ( ( i A k ) ( .r ` R ) ( k Z (/) ) ) ) ) )
29 snfi 
 |-  { (/) } e. Fin
30 29 a1i 
 |-  ( ( ph /\ i e. M ) -> { (/) } e. Fin )
31 9 adantr 
 |-  ( ( ph /\ i e. M ) -> Z e. ( B ^m ( N X. { (/) } ) ) )
32 0ex 
 |-  (/) e. _V
33 32 snid 
 |-  (/) e. { (/) }
34 33 a1i 
 |-  ( ( ph /\ i e. M ) -> (/) e. { (/) } )
35 1 3 10 11 12 13 30 14 31 16 34 mamufv 
 |-  ( ( ph /\ i e. M ) -> ( i ( A .X. Z ) (/) ) = ( R gsum ( k e. N |-> ( ( i A k ) ( .r ` R ) ( k Z (/) ) ) ) ) )
36 35 eqcomd 
 |-  ( ( ph /\ i e. M ) -> ( R gsum ( k e. N |-> ( ( i A k ) ( .r ` R ) ( k Z (/) ) ) ) ) = ( i ( A .X. Z ) (/) ) )
37 36 adantlr 
 |-  ( ( ( ph /\ A. j e. N ( Y ` j ) = ( j Z (/) ) ) /\ i e. M ) -> ( R gsum ( k e. N |-> ( ( i A k ) ( .r ` R ) ( k Z (/) ) ) ) ) = ( i ( A .X. Z ) (/) ) )
38 18 28 37 3eqtrd 
 |-  ( ( ( ph /\ A. j e. N ( Y ` j ) = ( j Z (/) ) ) /\ i e. M ) -> ( ( A .x. Y ) ` i ) = ( i ( A .X. Z ) (/) ) )
39 38 ralrimiva 
 |-  ( ( ph /\ A. j e. N ( Y ` j ) = ( j Z (/) ) ) -> A. i e. M ( ( A .x. Y ) ` i ) = ( i ( A .X. Z ) (/) ) )
40 39 ex 
 |-  ( ph -> ( A. j e. N ( Y ` j ) = ( j Z (/) ) -> A. i e. M ( ( A .x. Y ) ` i ) = ( i ( A .X. Z ) (/) ) ) )