Metamath Proof Explorer

Theorem matecl

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. (Contributed by AV, 16-Dec-2018)

Ref Expression
Hypotheses matecl.a 
|- A = ( N Mat R )
matecl.k 
|- K = ( Base ` R )
Assertion matecl 
|- ( ( I e. N /\ J e. N /\ M e. ( Base ` A ) ) -> ( I M J ) e. K )

Proof

Step Hyp Ref Expression
1 matecl.a 
 |-  A = ( N Mat R )
2 matecl.k 
 |-  K = ( Base ` R )
3 eqid 
 |-  ( Base ` A ) = ( Base ` A )
4 1 3 matrcl 
 |-  ( M e. ( Base ` A ) -> ( N e. Fin /\ R e. _V ) )
5 4 3ad2ant3 
 |-  ( ( I e. N /\ J e. N /\ M e. ( Base ` A ) ) -> ( N e. Fin /\ R e. _V ) )
6 1 2 matbas2 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )
7 6 eqcomd 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( Base ` A ) = ( K ^m ( N X. N ) ) )
8 7 eleq2d 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( M e. ( Base ` A ) <-> M e. ( K ^m ( N X. N ) ) ) )
9 2 fvexi 
 |-  K e. _V
10 9 a1i 
 |-  ( R e. _V -> K e. _V )
11 sqxpexg 
 |-  ( N e. Fin -> ( N X. N ) e. _V )
12 elmapg 
 |-  ( ( K e. _V /\ ( N X. N ) e. _V ) -> ( M e. ( K ^m ( N X. N ) ) <-> M : ( N X. N ) --> K ) )
13 10 11 12 syl2anr 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( M e. ( K ^m ( N X. N ) ) <-> M : ( N X. N ) --> K ) )
14 ffnov 
 |-  ( M : ( N X. N ) --> K <-> ( M Fn ( N X. N ) /\ A. i e. N A. j e. N ( i M j ) e. K ) )
15 oveq1 
 |-  ( i = I -> ( i M j ) = ( I M j ) )
16 15 eleq1d 
 |-  ( i = I -> ( ( i M j ) e. K <-> ( I M j ) e. K ) )
17 oveq2 
 |-  ( j = J -> ( I M j ) = ( I M J ) )
18 17 eleq1d 
 |-  ( j = J -> ( ( I M j ) e. K <-> ( I M J ) e. K ) )
19 16 18 rspc2v 
 |-  ( ( I e. N /\ J e. N ) -> ( A. i e. N A. j e. N ( i M j ) e. K -> ( I M J ) e. K ) )
20 19 com12 
 |-  ( A. i e. N A. j e. N ( i M j ) e. K -> ( ( I e. N /\ J e. N ) -> ( I M J ) e. K ) )
21 20 adantl 
 |-  ( ( M Fn ( N X. N ) /\ A. i e. N A. j e. N ( i M j ) e. K ) -> ( ( I e. N /\ J e. N ) -> ( I M J ) e. K ) )
22 21 a1i 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( ( M Fn ( N X. N ) /\ A. i e. N A. j e. N ( i M j ) e. K ) -> ( ( I e. N /\ J e. N ) -> ( I M J ) e. K ) ) )
23 14 22 syl5bi 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( M : ( N X. N ) --> K -> ( ( I e. N /\ J e. N ) -> ( I M J ) e. K ) ) )
24 13 23 sylbid 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( M e. ( K ^m ( N X. N ) ) -> ( ( I e. N /\ J e. N ) -> ( I M J ) e. K ) ) )
25 8 24 sylbid 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( M e. ( Base ` A ) -> ( ( I e. N /\ J e. N ) -> ( I M J ) e. K ) ) )
26 25 com13 
 |-  ( ( I e. N /\ J e. N ) -> ( M e. ( Base ` A ) -> ( ( N e. Fin /\ R e. _V ) -> ( I M J ) e. K ) ) )
27 26 ex 
 |-  ( I e. N -> ( J e. N -> ( M e. ( Base ` A ) -> ( ( N e. Fin /\ R e. _V ) -> ( I M J ) e. K ) ) ) )
28 27 3imp1 
 |-  ( ( ( I e. N /\ J e. N /\ M e. ( Base ` A ) ) /\ ( N e. Fin /\ R e. _V ) ) -> ( I M J ) e. K )
29 5 28 mpdan 
 |-  ( ( I e. N /\ J e. N /\ M e. ( Base ` A ) ) -> ( I M J ) e. K )