Metamath Proof Explorer

Theorem mamufv

Description: A cell in the multiplication of two matrices. (Contributed by Stefan O'Rear, 2-Sep-2015)

Ref Expression
Hypotheses mamufval.f 
|- F = ( R maMul <. M , N , P >. )
mamufval.b 
|- B = ( Base ` R )
mamufval.t 
|- .x. = ( .r ` R )
mamufval.r 
|- ( ph -> R e. V )
mamufval.m 
|- ( ph -> M e. Fin )
mamufval.n 
|- ( ph -> N e. Fin )
mamufval.p 
|- ( ph -> P e. Fin )
mamuval.x 
|- ( ph -> X e. ( B ^m ( M X. N ) ) )
mamuval.y 
|- ( ph -> Y e. ( B ^m ( N X. P ) ) )
mamufv.i 
|- ( ph -> I e. M )
mamufv.k 
|- ( ph -> K e. P )
Assertion mamufv 
|- ( ph -> ( I ( X F Y ) K ) = ( R gsum ( j e. N |-> ( ( I X j ) .x. ( j Y K ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mamufval.f 
 |-  F = ( R maMul <. M , N , P >. )
2 mamufval.b 
 |-  B = ( Base ` R )
3 mamufval.t 
 |-  .x. = ( .r ` R )
4 mamufval.r 
 |-  ( ph -> R e. V )
5 mamufval.m 
 |-  ( ph -> M e. Fin )
6 mamufval.n 
 |-  ( ph -> N e. Fin )
7 mamufval.p 
 |-  ( ph -> P e. Fin )
8 mamuval.x 
 |-  ( ph -> X e. ( B ^m ( M X. N ) ) )
9 mamuval.y 
 |-  ( ph -> Y e. ( B ^m ( N X. P ) ) )
10 mamufv.i 
 |-  ( ph -> I e. M )
11 mamufv.k 
 |-  ( ph -> K e. P )
12 1 2 3 4 5 6 7 8 9 mamuval 
 |-  ( ph -> ( X F Y ) = ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( j Y k ) ) ) ) ) )
13 oveq1 
 |-  ( i = I -> ( i X j ) = ( I X j ) )
14 oveq2 
 |-  ( k = K -> ( j Y k ) = ( j Y K ) )
15 13 14 oveqan12d 
 |-  ( ( i = I /\ k = K ) -> ( ( i X j ) .x. ( j Y k ) ) = ( ( I X j ) .x. ( j Y K ) ) )
16 15 adantl 
 |-  ( ( ph /\ ( i = I /\ k = K ) ) -> ( ( i X j ) .x. ( j Y k ) ) = ( ( I X j ) .x. ( j Y K ) ) )
17 16 mpteq2dv 
 |-  ( ( ph /\ ( i = I /\ k = K ) ) -> ( j e. N |-> ( ( i X j ) .x. ( j Y k ) ) ) = ( j e. N |-> ( ( I X j ) .x. ( j Y K ) ) ) )
18 17 oveq2d 
 |-  ( ( ph /\ ( i = I /\ k = K ) ) -> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( j Y k ) ) ) ) = ( R gsum ( j e. N |-> ( ( I X j ) .x. ( j Y K ) ) ) ) )
19 ovexd 
 |-  ( ph -> ( R gsum ( j e. N |-> ( ( I X j ) .x. ( j Y K ) ) ) ) e. _V )
20 12 18 10 11 19 ovmpod 
 |-  ( ph -> ( I ( X F Y ) K ) = ( R gsum ( j e. N |-> ( ( I X j ) .x. ( j Y K ) ) ) ) )