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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	matecl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	matecld.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	matecld.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
	matecld.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
	matecld.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
Assertion	matecld	⊢ ( 𝜑 → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		matecl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		matecl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		matecld.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		matecld.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
5		matecld.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
6		matecld.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
7	6 3	eleqtrdi	⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ 𝐴 ) )
8	1 2	matecl	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 )
9	4 5 7 8	syl3anc	⊢ ( 𝜑 → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 )