Metamath Proof Explorer


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 ) ) ) ) )