This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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