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 
|- ( 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 )