This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 Mat R$
	matecl.k	$⊢ K = {Base}_{R}$
	matecld.b	$⊢ B = {Base}_{A}$
	matecld.i	$⊢ φ \to I \in N$
	matecld.j	$⊢ φ \to J \in N$
	matecld.m	$⊢ φ \to M \in B$
Assertion	matecld	$⊢ φ \to I M J \in 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	$⊢ φ \to I \in N$
5		matecld.j	$⊢ φ \to J \in N$
6		matecld.m	$⊢ φ \to M \in B$
7	6 3	eleqtrdi	$⊢ φ \to M \in {Base}_{A}$
8	1 2	matecl	$⊢ (I \in N \land J \in N \land M \in {Base}_{A}) \to I M J \in K$
9	4 5 7 8	syl3anc	$⊢ φ \to I M J \in K$