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 φ R Ring
mamucl.f F = R maMul M N P
mamucl.m φ M Fin
mamucl.n φ N Fin
mamucl.p φ P Fin
mamucl.x φ X B M × N
mamucl.y φ Y B N × P
Assertion mamucl φ X F Y B M × P

Proof

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