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