# Metamath Proof Explorer

## Theorem matmulcell

Description: Multiplication in the matrix ring for a single cell of a matrix. (Contributed by AV, 17-Nov-2019) (Revised by AV, 3-Jul-2022)

Ref Expression
Hypotheses matmulcell.a
`|- A = ( N Mat R )`
matmulcell.b
`|- B = ( Base ` A )`
matmulcell.m
`|- .X. = ( .r ` A )`
Assertion matmulcell
`|- ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( X .X. Y ) J ) = ( R gsum ( j e. N |-> ( ( I X j ) ( .r ` R ) ( j Y J ) ) ) ) )`

### Proof

Step Hyp Ref Expression
1 matmulcell.a
` |-  A = ( N Mat R )`
2 matmulcell.b
` |-  B = ( Base ` A )`
3 matmulcell.m
` |-  .X. = ( .r ` A )`
4 1 2 matrcl
` |-  ( X e. B -> ( N e. Fin /\ R e. _V ) )`
5 eqid
` |-  ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )`
6 1 5 matmulr
` |-  ( ( N e. Fin /\ R e. _V ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )`
7 3 6 eqtr4id
` |-  ( ( N e. Fin /\ R e. _V ) -> .X. = ( R maMul <. N , N , N >. ) )`
8 7 a1d
` |-  ( ( N e. Fin /\ R e. _V ) -> ( R e. Ring -> .X. = ( R maMul <. N , N , N >. ) ) )`
9 4 8 syl
` |-  ( X e. B -> ( R e. Ring -> .X. = ( R maMul <. N , N , N >. ) ) )`
` |-  ( ( X e. B /\ Y e. B ) -> ( R e. Ring -> .X. = ( R maMul <. N , N , N >. ) ) )`
11 10 impcom
` |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) ) -> .X. = ( R maMul <. N , N , N >. ) )`
` |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> .X. = ( R maMul <. N , N , N >. ) )`
13 12 oveqd
` |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( X .X. Y ) = ( X ( R maMul <. N , N , N >. ) Y ) )`
14 13 oveqd
` |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( X .X. Y ) J ) = ( I ( X ( R maMul <. N , N , N >. ) Y ) J ) )`
15 eqid
` |-  ( Base ` R ) = ( Base ` R )`
16 eqid
` |-  ( .r ` R ) = ( .r ` R )`
17 simp1
` |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> R e. Ring )`
18 4 simpld
` |-  ( X e. B -> N e. Fin )`
` |-  ( ( X e. B /\ Y e. B ) -> N e. Fin )`
` |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> N e. Fin )`
21 1 15 2 matbas2i
` |-  ( X e. B -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )`
` |-  ( ( X e. B /\ Y e. B ) -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )`
` |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )`
24 1 15 2 matbas2i
` |-  ( Y e. B -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) )`
` |-  ( ( X e. B /\ Y e. B ) -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) )`
` |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) )`
` |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> I e. N )`
` |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> J e. N )`
` |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( X ( R maMul <. N , N , N >. ) Y ) J ) = ( R gsum ( j e. N |-> ( ( I X j ) ( .r ` R ) ( j Y J ) ) ) ) )`
` |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( X .X. Y ) J ) = ( R gsum ( j e. N |-> ( ( I X j ) ( .r ` R ) ( j Y J ) ) ) ) )`