Metamath Proof Explorer

Theorem mamucl

Description: Operation closure of matrix multiplication. (Contributed by Stefan O'Rear, 2-Sep-2015) (Proof shortened by AV, 23-Jul-2019)

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

Proof

Step Hyp Ref Expression
1 mamucl.b 
 |-  B = ( Base ` R )
2 mamucl.r 
 |-  ( ph -> R e. Ring )
3 mamucl.f 
 |-  F = ( R maMul <. M , N , P >. )
4 mamucl.m 
 |-  ( ph -> M e. Fin )
5 mamucl.n 
 |-  ( ph -> N e. Fin )
6 mamucl.p 
 |-  ( ph -> P e. Fin )
7 mamucl.x 
 |-  ( ph -> X e. ( B ^m ( M X. N ) ) )
8 mamucl.y 
 |-  ( ph -> Y e. ( B ^m ( N X. P ) ) )
9 eqid 
 |-  ( .r ` R ) = ( .r ` R )
10 3 1 9 2 4 5 6 7 8 mamuval 
 |-  ( ph -> ( X F Y ) = ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Y k ) ) ) ) ) )
11 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
12 2 11 syl 
 |-  ( ph -> R e. CMnd )
13 12 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> R e. CMnd )
14 5 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> N e. Fin )
15 2 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. N ) -> R e. Ring )
16 elmapi 
 |-  ( X e. ( B ^m ( M X. N ) ) -> X : ( M X. N ) --> B )
17 7 16 syl 
 |-  ( ph -> X : ( M X. N ) --> B )
18 17 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. N ) -> X : ( M X. N ) --> B )
19 simplrl 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. N ) -> i e. M )
20 simpr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. N ) -> j e. N )
21 18 19 20 fovcdmd 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. N ) -> ( i X j ) e. B )
22 elmapi 
 |-  ( Y e. ( B ^m ( N X. P ) ) -> Y : ( N X. P ) --> B )
23 8 22 syl 
 |-  ( ph -> Y : ( N X. P ) --> B )
24 23 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. N ) -> Y : ( N X. P ) --> B )
25 simplrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. N ) -> k e. P )
26 24 20 25 fovcdmd 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. N ) -> ( j Y k ) e. B )
27 1 9 ringcl 
 |-  ( ( R e. Ring /\ ( i X j ) e. B /\ ( j Y k ) e. B ) -> ( ( i X j ) ( .r ` R ) ( j Y k ) ) e. B )
28 15 21 26 27 syl3anc 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. N ) -> ( ( i X j ) ( .r ` R ) ( j Y k ) ) e. B )
29 28 ralrimiva 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> A. j e. N ( ( i X j ) ( .r ` R ) ( j Y k ) ) e. B )
30 1 13 14 29 gsummptcl 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Y k ) ) ) ) e. B )
31 30 ralrimivva 
 |-  ( ph -> A. i e. M A. k e. P ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Y k ) ) ) ) e. B )
32 eqid 
 |-  ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Y k ) ) ) ) ) = ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Y k ) ) ) ) )
33 32 fmpo 
 |-  ( A. i e. M A. k e. P ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Y k ) ) ) ) e. B <-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Y k ) ) ) ) ) : ( M X. P ) --> B )
34 1 fvexi 
 |-  B e. _V
35 xpfi 
 |-  ( ( M e. Fin /\ P e. Fin ) -> ( M X. P ) e. Fin )
36 4 6 35 syl2anc 
 |-  ( ph -> ( M X. P ) e. Fin )
37 elmapg 
 |-  ( ( B e. _V /\ ( M X. P ) e. Fin ) -> ( ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Y k ) ) ) ) ) e. ( B ^m ( M X. P ) ) <-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Y k ) ) ) ) ) : ( M X. P ) --> B ) )
38 34 36 37 sylancr 
 |-  ( ph -> ( ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Y k ) ) ) ) ) e. ( B ^m ( M X. P ) ) <-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Y k ) ) ) ) ) : ( M X. P ) --> B ) )
39 33 38 bitr4id 
 |-  ( ph -> ( A. i e. M A. k e. P ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Y k ) ) ) ) e. B <-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Y k ) ) ) ) ) e. ( B ^m ( M X. P ) ) ) )
40 31 39 mpbid 
 |-  ( ph -> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Y k ) ) ) ) ) e. ( B ^m ( M X. P ) ) )
41 10 40 eqeltrd 
 |-  ( ph -> ( X F Y ) e. ( B ^m ( M X. P ) ) )