Metamath Proof Explorer

Theorem mamures

Description: Rows in a matrix product are functions only of the corresponding rows in the left argument. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses mamures.f 
|- F = ( R maMul <. M , N , P >. )
mamures.g 
|- G = ( R maMul <. I , N , P >. )
mamures.b 
|- B = ( Base ` R )
mamures.r 
|- ( ph -> R e. V )
mamures.m 
|- ( ph -> M e. Fin )
mamures.n 
|- ( ph -> N e. Fin )
mamures.p 
|- ( ph -> P e. Fin )
mamures.i 
|- ( ph -> I C_ M )
mamures.x 
|- ( ph -> X e. ( B ^m ( M X. N ) ) )
mamures.y 
|- ( ph -> Y e. ( B ^m ( N X. P ) ) )
Assertion mamures 
|- ( ph -> ( ( X F Y ) |` ( I X. P ) ) = ( ( X |` ( I X. N ) ) G Y ) )

Proof

Step Hyp Ref Expression
1 mamures.f 
 |-  F = ( R maMul <. M , N , P >. )
2 mamures.g 
 |-  G = ( R maMul <. I , N , P >. )
3 mamures.b 
 |-  B = ( Base ` R )
4 mamures.r 
 |-  ( ph -> R e. V )
5 mamures.m 
 |-  ( ph -> M e. Fin )
6 mamures.n 
 |-  ( ph -> N e. Fin )
7 mamures.p 
 |-  ( ph -> P e. Fin )
8 mamures.i 
 |-  ( ph -> I C_ M )
9 mamures.x 
 |-  ( ph -> X e. ( B ^m ( M X. N ) ) )
10 mamures.y 
 |-  ( ph -> Y e. ( B ^m ( N X. P ) ) )
11 ssidd 
 |-  ( ph -> P C_ P )
12 resmpo 
 |-  ( ( I C_ M /\ P C_ P ) -> ( ( i e. M , j e. P |-> ( R gsum ( k e. N |-> ( ( i X k ) ( .r ` R ) ( k Y j ) ) ) ) ) |` ( I X. P ) ) = ( i e. I , j e. P |-> ( R gsum ( k e. N |-> ( ( i X k ) ( .r ` R ) ( k Y j ) ) ) ) ) )
13 8 11 12 syl2anc 
 |-  ( ph -> ( ( i e. M , j e. P |-> ( R gsum ( k e. N |-> ( ( i X k ) ( .r ` R ) ( k Y j ) ) ) ) ) |` ( I X. P ) ) = ( i e. I , j e. P |-> ( R gsum ( k e. N |-> ( ( i X k ) ( .r ` R ) ( k Y j ) ) ) ) ) )
14 ovres 
 |-  ( ( i e. I /\ k e. N ) -> ( i ( X |` ( I X. N ) ) k ) = ( i X k ) )
15 14 3ad2antl2 
 |-  ( ( ( ph /\ i e. I /\ j e. P ) /\ k e. N ) -> ( i ( X |` ( I X. N ) ) k ) = ( i X k ) )
16 15 eqcomd 
 |-  ( ( ( ph /\ i e. I /\ j e. P ) /\ k e. N ) -> ( i X k ) = ( i ( X |` ( I X. N ) ) k ) )
17 16 oveq1d 
 |-  ( ( ( ph /\ i e. I /\ j e. P ) /\ k e. N ) -> ( ( i X k ) ( .r ` R ) ( k Y j ) ) = ( ( i ( X |` ( I X. N ) ) k ) ( .r ` R ) ( k Y j ) ) )
18 17 mpteq2dva 
 |-  ( ( ph /\ i e. I /\ j e. P ) -> ( k e. N |-> ( ( i X k ) ( .r ` R ) ( k Y j ) ) ) = ( k e. N |-> ( ( i ( X |` ( I X. N ) ) k ) ( .r ` R ) ( k Y j ) ) ) )
19 18 oveq2d 
 |-  ( ( ph /\ i e. I /\ j e. P ) -> ( R gsum ( k e. N |-> ( ( i X k ) ( .r ` R ) ( k Y j ) ) ) ) = ( R gsum ( k e. N |-> ( ( i ( X |` ( I X. N ) ) k ) ( .r ` R ) ( k Y j ) ) ) ) )
20 19 mpoeq3dva 
 |-  ( ph -> ( i e. I , j e. P |-> ( R gsum ( k e. N |-> ( ( i X k ) ( .r ` R ) ( k Y j ) ) ) ) ) = ( i e. I , j e. P |-> ( R gsum ( k e. N |-> ( ( i ( X |` ( I X. N ) ) k ) ( .r ` R ) ( k Y j ) ) ) ) ) )
21 13 20 eqtrd 
 |-  ( ph -> ( ( i e. M , j e. P |-> ( R gsum ( k e. N |-> ( ( i X k ) ( .r ` R ) ( k Y j ) ) ) ) ) |` ( I X. P ) ) = ( i e. I , j e. P |-> ( R gsum ( k e. N |-> ( ( i ( X |` ( I X. N ) ) k ) ( .r ` R ) ( k Y j ) ) ) ) ) )
22 eqid 
 |-  ( .r ` R ) = ( .r ` R )
23 1 3 22 4 5 6 7 9 10 mamuval 
 |-  ( ph -> ( X F Y ) = ( i e. M , j e. P |-> ( R gsum ( k e. N |-> ( ( i X k ) ( .r ` R ) ( k Y j ) ) ) ) ) )
24 23 reseq1d 
 |-  ( ph -> ( ( X F Y ) |` ( I X. P ) ) = ( ( i e. M , j e. P |-> ( R gsum ( k e. N |-> ( ( i X k ) ( .r ` R ) ( k Y j ) ) ) ) ) |` ( I X. P ) ) )
25 5 8 ssfid 
 |-  ( ph -> I e. Fin )
26 elmapi 
 |-  ( X e. ( B ^m ( M X. N ) ) -> X : ( M X. N ) --> B )
27 9 26 syl 
 |-  ( ph -> X : ( M X. N ) --> B )
28 xpss1 
 |-  ( I C_ M -> ( I X. N ) C_ ( M X. N ) )
29 8 28 syl 
 |-  ( ph -> ( I X. N ) C_ ( M X. N ) )
30 27 29 fssresd 
 |-  ( ph -> ( X |` ( I X. N ) ) : ( I X. N ) --> B )
31 3 fvexi 
 |-  B e. _V
32 31 a1i 
 |-  ( ph -> B e. _V )
33 xpfi 
 |-  ( ( I e. Fin /\ N e. Fin ) -> ( I X. N ) e. Fin )
34 25 6 33 syl2anc 
 |-  ( ph -> ( I X. N ) e. Fin )
35 32 34 elmapd 
 |-  ( ph -> ( ( X |` ( I X. N ) ) e. ( B ^m ( I X. N ) ) <-> ( X |` ( I X. N ) ) : ( I X. N ) --> B ) )
36 30 35 mpbird 
 |-  ( ph -> ( X |` ( I X. N ) ) e. ( B ^m ( I X. N ) ) )
37 2 3 22 4 25 6 7 36 10 mamuval 
 |-  ( ph -> ( ( X |` ( I X. N ) ) G Y ) = ( i e. I , j e. P |-> ( R gsum ( k e. N |-> ( ( i ( X |` ( I X. N ) ) k ) ( .r ` R ) ( k Y j ) ) ) ) ) )
38 21 24 37 3eqtr4d 
 |-  ( ph -> ( ( X F Y ) |` ( I X. P ) ) = ( ( X |` ( I X. N ) ) G Y ) )