# 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}={\mathrm{Base}}_{{R}}$
mamucl.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
mamucl.f ${⊢}{F}={R}\mathrm{maMul}⟨{M},{N},{P}⟩$
mamucl.m ${⊢}{\phi }\to {M}\in \mathrm{Fin}$
mamucl.n ${⊢}{\phi }\to {N}\in \mathrm{Fin}$
mamucl.p ${⊢}{\phi }\to {P}\in \mathrm{Fin}$
mamucl.x ${⊢}{\phi }\to {X}\in \left({{B}}^{\left({M}×{N}\right)}\right)$
mamucl.y ${⊢}{\phi }\to {Y}\in \left({{B}}^{\left({N}×{P}\right)}\right)$
Assertion mamucl ${⊢}{\phi }\to {X}{F}{Y}\in \left({{B}}^{\left({M}×{P}\right)}\right)$

### Proof

Step Hyp Ref Expression
1 mamucl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 mamucl.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
3 mamucl.f ${⊢}{F}={R}\mathrm{maMul}⟨{M},{N},{P}⟩$
4 mamucl.m ${⊢}{\phi }\to {M}\in \mathrm{Fin}$
5 mamucl.n ${⊢}{\phi }\to {N}\in \mathrm{Fin}$
6 mamucl.p ${⊢}{\phi }\to {P}\in \mathrm{Fin}$
7 mamucl.x ${⊢}{\phi }\to {X}\in \left({{B}}^{\left({M}×{N}\right)}\right)$
8 mamucl.y ${⊢}{\phi }\to {Y}\in \left({{B}}^{\left({N}×{P}\right)}\right)$
9 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
10 3 1 9 2 4 5 6 7 8 mamuval ${⊢}{\phi }\to {X}{F}{Y}=\left({i}\in {M},{k}\in {P}⟼\underset{{j}\in {N}}{{\sum }_{{R}}}\left(\left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\right)\right)$
11 ringcmn ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{CMnd}$
12 2 11 syl ${⊢}{\phi }\to {R}\in \mathrm{CMnd}$
13 12 adantr ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {P}\right)\right)\to {R}\in \mathrm{CMnd}$
14 5 adantr ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {P}\right)\right)\to {N}\in \mathrm{Fin}$
15 2 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {P}\right)\right)\wedge {j}\in {N}\right)\to {R}\in \mathrm{Ring}$
16 elmapi ${⊢}{X}\in \left({{B}}^{\left({M}×{N}\right)}\right)\to {X}:{M}×{N}⟶{B}$
17 7 16 syl ${⊢}{\phi }\to {X}:{M}×{N}⟶{B}$
18 17 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {P}\right)\right)\wedge {j}\in {N}\right)\to {X}:{M}×{N}⟶{B}$
19 simplrl ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {P}\right)\right)\wedge {j}\in {N}\right)\to {i}\in {M}$
20 simpr ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {P}\right)\right)\wedge {j}\in {N}\right)\to {j}\in {N}$
21 18 19 20 fovrnd ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {P}\right)\right)\wedge {j}\in {N}\right)\to {i}{X}{j}\in {B}$
22 elmapi ${⊢}{Y}\in \left({{B}}^{\left({N}×{P}\right)}\right)\to {Y}:{N}×{P}⟶{B}$
23 8 22 syl ${⊢}{\phi }\to {Y}:{N}×{P}⟶{B}$
24 23 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {P}\right)\right)\wedge {j}\in {N}\right)\to {Y}:{N}×{P}⟶{B}$
25 simplrr ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {P}\right)\right)\wedge {j}\in {N}\right)\to {k}\in {P}$
26 24 20 25 fovrnd ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {P}\right)\right)\wedge {j}\in {N}\right)\to {j}{Y}{k}\in {B}$
27 1 9 ringcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {i}{X}{j}\in {B}\wedge {j}{Y}{k}\in {B}\right)\to \left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\in {B}$
28 15 21 26 27 syl3anc ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {P}\right)\right)\wedge {j}\in {N}\right)\to \left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\in {B}$
29 28 ralrimiva ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {P}\right)\right)\to \forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\in {B}$
30 1 13 14 29 gsummptcl ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {P}\right)\right)\to \underset{{j}\in {N}}{{\sum }_{{R}}}\left(\left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\right)\in {B}$
31 30 ralrimivva ${⊢}{\phi }\to \forall {i}\in {M}\phantom{\rule{.4em}{0ex}}\forall {k}\in {P}\phantom{\rule{.4em}{0ex}}\underset{{j}\in {N}}{{\sum }_{{R}}}\left(\left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\right)\in {B}$
32 1 fvexi ${⊢}{B}\in \mathrm{V}$
33 xpfi ${⊢}\left({M}\in \mathrm{Fin}\wedge {P}\in \mathrm{Fin}\right)\to {M}×{P}\in \mathrm{Fin}$
34 4 6 33 syl2anc ${⊢}{\phi }\to {M}×{P}\in \mathrm{Fin}$
35 elmapg ${⊢}\left({B}\in \mathrm{V}\wedge {M}×{P}\in \mathrm{Fin}\right)\to \left(\left({i}\in {M},{k}\in {P}⟼\underset{{j}\in {N}}{{\sum }_{{R}}}\left(\left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\right)\right)\in \left({{B}}^{\left({M}×{P}\right)}\right)↔\left({i}\in {M},{k}\in {P}⟼\underset{{j}\in {N}}{{\sum }_{{R}}}\left(\left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\right)\right):{M}×{P}⟶{B}\right)$
36 32 34 35 sylancr ${⊢}{\phi }\to \left(\left({i}\in {M},{k}\in {P}⟼\underset{{j}\in {N}}{{\sum }_{{R}}}\left(\left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\right)\right)\in \left({{B}}^{\left({M}×{P}\right)}\right)↔\left({i}\in {M},{k}\in {P}⟼\underset{{j}\in {N}}{{\sum }_{{R}}}\left(\left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\right)\right):{M}×{P}⟶{B}\right)$
37 eqid ${⊢}\left({i}\in {M},{k}\in {P}⟼\underset{{j}\in {N}}{{\sum }_{{R}}}\left(\left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\right)\right)=\left({i}\in {M},{k}\in {P}⟼\underset{{j}\in {N}}{{\sum }_{{R}}}\left(\left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\right)\right)$
38 37 fmpo ${⊢}\forall {i}\in {M}\phantom{\rule{.4em}{0ex}}\forall {k}\in {P}\phantom{\rule{.4em}{0ex}}\underset{{j}\in {N}}{{\sum }_{{R}}}\left(\left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\right)\in {B}↔\left({i}\in {M},{k}\in {P}⟼\underset{{j}\in {N}}{{\sum }_{{R}}}\left(\left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\right)\right):{M}×{P}⟶{B}$
39 36 38 syl6rbbr ${⊢}{\phi }\to \left(\forall {i}\in {M}\phantom{\rule{.4em}{0ex}}\forall {k}\in {P}\phantom{\rule{.4em}{0ex}}\underset{{j}\in {N}}{{\sum }_{{R}}}\left(\left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\right)\in {B}↔\left({i}\in {M},{k}\in {P}⟼\underset{{j}\in {N}}{{\sum }_{{R}}}\left(\left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\right)\right)\in \left({{B}}^{\left({M}×{P}\right)}\right)\right)$
40 31 39 mpbid ${⊢}{\phi }\to \left({i}\in {M},{k}\in {P}⟼\underset{{j}\in {N}}{{\sum }_{{R}}}\left(\left({i}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{k}\right)\right)\right)\in \left({{B}}^{\left({M}×{P}\right)}\right)$
41 10 40 eqeltrd ${⊢}{\phi }\to {X}{F}{Y}\in \left({{B}}^{\left({M}×{P}\right)}\right)$