Metamath Proof Explorer

Theorem matecld

Description: Each entry (according to Wikipedia "Matrix (mathematics)", 30-Dec-2018, (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 Mat R
matecl.k K = Base R
matecld.b B = Base A
matecld.i φ I N
matecld.j φ J N
matecld.m φ M B
Assertion matecld φ I M J K


Step Hyp Ref Expression
1 matecl.a A = N Mat R
2 matecl.k K = Base R
3 matecld.b B = Base A
4 matecld.i φ I N
5 matecld.j φ J N
6 matecld.m φ M B
7 6 3 eleqtrdi φ M Base A
8 1 2 matecl I N J N M Base A I M J K
9 4 5 7 8 syl3anc φ I M J K