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 IMJ\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 IMJ\in K$$
9	4 5 7 8	syl3anc	$$⊢\phi \to IMJ\in K$$