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 Mat R )
	matecl.k	|- K = ( Base ` R )
	matecld.b	|- B = ( Base ` A )
	matecld.i	|- ( ph -> I e. N )
	matecld.j	|- ( ph -> J e. N )
	matecld.m	|- ( ph -> M e. B )
Assertion	matecld	|- ( ph -> ( I M J ) e. K )

Proof

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	|- ( ph -> I e. N )
5		matecld.j	|- ( ph -> J e. N )
6		matecld.m	|- ( ph -> M e. B )
7	6 3	eleqtrdi	|- ( ph -> M e. ( Base ` A ) )
8	1 2	matecl	|- ( ( I e. N /\ J e. N /\ M e. ( Base ` A ) ) -> ( I M J ) e. K )
9	4 5 7 8	syl3anc	|- ( ph -> ( I M J ) e. K )