# Metamath Proof Explorer

## Theorem matecld

Description: Each entry (according to Wikipedia "Matrix (mathematics)", 30-Dec-2018, https://en.wikipedia.org/wiki/Matrix_(mathematics)#Definition (or element or component or coefficient or cell) of a matrix is an element of the underlying ring, deduction form. (Contributed by AV, 27-Nov-2019)

Ref Expression
Hypotheses matecl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
matecl.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
matecld.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
matecld.i ${⊢}{\phi }\to {I}\in {N}$
matecld.j ${⊢}{\phi }\to {J}\in {N}$
matecld.m ${⊢}{\phi }\to {M}\in {B}$
Assertion matecld ${⊢}{\phi }\to {I}{M}{J}\in {K}$

### Proof

Step Hyp Ref Expression
1 matecl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 matecl.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
3 matecld.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
4 matecld.i ${⊢}{\phi }\to {I}\in {N}$
5 matecld.j ${⊢}{\phi }\to {J}\in {N}$
6 matecld.m ${⊢}{\phi }\to {M}\in {B}$
7 6 3 eleqtrdi ${⊢}{\phi }\to {M}\in {\mathrm{Base}}_{{A}}$
8 1 2 matecl ${⊢}\left({I}\in {N}\wedge {J}\in {N}\wedge {M}\in {\mathrm{Base}}_{{A}}\right)\to {I}{M}{J}\in {K}$
9 4 5 7 8 syl3anc ${⊢}{\phi }\to {I}{M}{J}\in {K}$