Metamath Proof Explorer

Theorem matvscacell

Description: Scalar multiplication in the matrix ring is cell-wise. (Contributed by AV, 7-Aug-2019)

Ref Expression
Hypotheses matplusgcell.a 
|- A = ( N Mat R )
matplusgcell.b 
|- B = ( Base ` A )
matvscacell.k 
|- K = ( Base ` R )
matvscacell.v 
|- .x. = ( .s ` A )
matvscacell.t 
|- .X. = ( .r ` R )
Assertion matvscacell 
|- ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( X .x. Y ) J ) = ( X .X. ( I Y J ) ) )

Proof

Step Hyp Ref Expression
1 matplusgcell.a 
 |-  A = ( N Mat R )
2 matplusgcell.b 
 |-  B = ( Base ` A )
3 matvscacell.k 
 |-  K = ( Base ` R )
4 matvscacell.v 
 |-  .x. = ( .s ` A )
5 matvscacell.t 
 |-  .X. = ( .r ` R )
6 eqid 
 |-  ( N X. N ) = ( N X. N )
7 1 2 3 4 5 6 matvsca2 
 |-  ( ( X e. K /\ Y e. B ) -> ( X .x. Y ) = ( ( ( N X. N ) X. { X } ) oF .X. Y ) )
8 7 oveqd 
 |-  ( ( X e. K /\ Y e. B ) -> ( I ( X .x. Y ) J ) = ( I ( ( ( N X. N ) X. { X } ) oF .X. Y ) J ) )
9 8 3ad2ant2 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( X .x. Y ) J ) = ( I ( ( ( N X. N ) X. { X } ) oF .X. Y ) J ) )
10 df-ov 
 |-  ( I ( ( ( N X. N ) X. { X } ) oF .X. Y ) J ) = ( ( ( ( N X. N ) X. { X } ) oF .X. Y ) ` <. I , J >. )
11 10 a1i 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( ( ( N X. N ) X. { X } ) oF .X. Y ) J ) = ( ( ( ( N X. N ) X. { X } ) oF .X. Y ) ` <. I , J >. ) )
12 opelxpi 
 |-  ( ( I e. N /\ J e. N ) -> <. I , J >. e. ( N X. N ) )
13 12 3ad2ant3 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> <. I , J >. e. ( N X. N ) )
14 1 2 matrcl 
 |-  ( Y e. B -> ( N e. Fin /\ R e. _V ) )
15 14 simpld 
 |-  ( Y e. B -> N e. Fin )
16 15 adantl 
 |-  ( ( X e. K /\ Y e. B ) -> N e. Fin )
17 16 3ad2ant2 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> N e. Fin )
18 xpfi 
 |-  ( ( N e. Fin /\ N e. Fin ) -> ( N X. N ) e. Fin )
19 17 17 18 syl2anc 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( N X. N ) e. Fin )
20 simp2l 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> X e. K )
21 2 eleq2i 
 |-  ( Y e. B <-> Y e. ( Base ` A ) )
22 21 biimpi 
 |-  ( Y e. B -> Y e. ( Base ` A ) )
23 22 adantl 
 |-  ( ( X e. K /\ Y e. B ) -> Y e. ( Base ` A ) )
24 23 3ad2ant2 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> Y e. ( Base ` A ) )
25 simp1 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> R e. Ring )
26 eqid 
 |-  ( Base ` R ) = ( Base ` R )
27 1 26 matbas2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( Base ` R ) ^m ( N X. N ) ) = ( Base ` A ) )
28 17 25 27 syl2anc 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( ( Base ` R ) ^m ( N X. N ) ) = ( Base ` A ) )
29 24 28 eleqtrrd 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) )
30 elmapfn 
 |-  ( Y e. ( ( Base ` R ) ^m ( N X. N ) ) -> Y Fn ( N X. N ) )
31 29 30 syl 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> Y Fn ( N X. N ) )
32 df-ov 
 |-  ( I Y J ) = ( Y ` <. I , J >. )
33 32 eqcomi 
 |-  ( Y ` <. I , J >. ) = ( I Y J )
34 33 a1i 
 |-  ( ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) /\ <. I , J >. e. ( N X. N ) ) -> ( Y ` <. I , J >. ) = ( I Y J ) )
35 19 20 31 34 ofc1 
 |-  ( ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) /\ <. I , J >. e. ( N X. N ) ) -> ( ( ( ( N X. N ) X. { X } ) oF .X. Y ) ` <. I , J >. ) = ( X .X. ( I Y J ) ) )
36 13 35 mpdan 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( ( ( ( N X. N ) X. { X } ) oF .X. Y ) ` <. I , J >. ) = ( X .X. ( I Y J ) ) )
37 9 11 36 3eqtrd 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( X .x. Y ) J ) = ( X .X. ( I Y J ) ) )