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

Metamath Proof Explorer

Theorem mamuval

Description: 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 ) ) )
Assertion mamuval 
|- ( ph -> ( X F Y ) = ( i e. M , k e. P |-> ( 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 1 2 3 4 5 6 7 mamufval 
 |-  ( ph -> F = ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m ( N X. P ) ) |-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( j y k ) ) ) ) ) ) )
11 oveq 
 |-  ( x = X -> ( i x j ) = ( i X j ) )
12 oveq 
 |-  ( y = Y -> ( j y k ) = ( j Y k ) )
13 11 12 oveqan12d 
 |-  ( ( x = X /\ y = Y ) -> ( ( i x j ) .x. ( j y k ) ) = ( ( i X j ) .x. ( j Y k ) ) )
14 13 adantl 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( i x j ) .x. ( j y k ) ) = ( ( i X j ) .x. ( j Y k ) ) )
15 14 mpteq2dv 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( j e. N |-> ( ( i x j ) .x. ( j y k ) ) ) = ( j e. N |-> ( ( i X j ) .x. ( j Y k ) ) ) )
16 15 oveq2d 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( j y k ) ) ) ) = ( R gsum ( j e. N |-> ( ( i X j ) .x. ( j Y k ) ) ) ) )
17 16 mpoeq3dv 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( j y k ) ) ) ) ) = ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( j Y k ) ) ) ) ) )
18 mpoexga 
 |-  ( ( M e. Fin /\ P e. Fin ) -> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( j Y k ) ) ) ) ) e. _V )
19 5 7 18 syl2anc 
 |-  ( ph -> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( j Y k ) ) ) ) ) e. _V )
20 10 17 8 9 19 ovmpod 
 |-  ( ph -> ( X F Y ) = ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( j Y k ) ) ) ) ) )