# Metamath Proof Explorer

## Theorem mulmarep1gsum1

Description: The sum of element by element multiplications of a matrix with an identity matrix with a column replaced by a vector. (Contributed by AV, 16-Feb-2019) (Revised by AV, 26-Feb-2019)

Ref Expression
Hypotheses marepvcl.a
`|- A = ( N Mat R )`
marepvcl.b
`|- B = ( Base ` A )`
marepvcl.v
`|- V = ( ( Base ` R ) ^m N )`
ma1repvcl.1
`|- .1. = ( 1r ` A )`
mulmarep1el.0
`|- .0. = ( 0g ` R )`
mulmarep1el.e
`|- E = ( ( .1. ( N matRepV R ) C ) ` K )`
Assertion mulmarep1gsum1
`|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> ( R gsum ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = ( I X J ) )`

### Proof

Step Hyp Ref Expression
1 marepvcl.a
` |-  A = ( N Mat R )`
2 marepvcl.b
` |-  B = ( Base ` A )`
3 marepvcl.v
` |-  V = ( ( Base ` R ) ^m N )`
4 ma1repvcl.1
` |-  .1. = ( 1r ` A )`
5 mulmarep1el.0
` |-  .0. = ( 0g ` R )`
6 mulmarep1el.e
` |-  E = ( ( .1. ( N matRepV R ) C ) ` K )`
7 simp1
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> R e. Ring )`
` |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) /\ l e. N ) -> R e. Ring )`
9 simp2
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> ( X e. B /\ C e. V /\ K e. N ) )`
` |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) /\ l e. N ) -> ( X e. B /\ C e. V /\ K e. N ) )`
11 simp1
` |-  ( ( I e. N /\ J e. N /\ J =/= K ) -> I e. N )`
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> I e. N )`
` |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) /\ l e. N ) -> I e. N )`
14 simp2
` |-  ( ( I e. N /\ J e. N /\ J =/= K ) -> J e. N )`
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> J e. N )`
` |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) /\ l e. N ) -> J e. N )`
17 simpr
` |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) /\ l e. N ) -> l e. N )`
18 1 2 3 4 5 6 mulmarep1el
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ l e. N ) ) -> ( ( I X l ) ( .r ` R ) ( l E J ) ) = if ( J = K , ( ( I X l ) ( .r ` R ) ( C ` l ) ) , if ( J = l , ( I X l ) , .0. ) ) )`
19 8 10 13 16 17 18 syl113anc
` |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) /\ l e. N ) -> ( ( I X l ) ( .r ` R ) ( l E J ) ) = if ( J = K , ( ( I X l ) ( .r ` R ) ( C ` l ) ) , if ( J = l , ( I X l ) , .0. ) ) )`
20 19 mpteq2dva
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) = ( l e. N |-> if ( J = K , ( ( I X l ) ( .r ` R ) ( C ` l ) ) , if ( J = l , ( I X l ) , .0. ) ) ) )`
21 20 oveq2d
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> ( R gsum ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = ( R gsum ( l e. N |-> if ( J = K , ( ( I X l ) ( .r ` R ) ( C ` l ) ) , if ( J = l , ( I X l ) , .0. ) ) ) ) )`
22 neneq
` |-  ( J =/= K -> -. J = K )`
` |-  ( ( I e. N /\ J e. N /\ J =/= K ) -> -. J = K )`
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> -. J = K )`
25 24 iffalsed
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> if ( J = K , ( ( I X l ) ( .r ` R ) ( C ` l ) ) , if ( J = l , ( I X l ) , .0. ) ) = if ( J = l , ( I X l ) , .0. ) )`
26 25 mpteq2dv
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> ( l e. N |-> if ( J = K , ( ( I X l ) ( .r ` R ) ( C ` l ) ) , if ( J = l , ( I X l ) , .0. ) ) ) = ( l e. N |-> if ( J = l , ( I X l ) , .0. ) ) )`
27 26 oveq2d
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> ( R gsum ( l e. N |-> if ( J = K , ( ( I X l ) ( .r ` R ) ( C ` l ) ) , if ( J = l , ( I X l ) , .0. ) ) ) ) = ( R gsum ( l e. N |-> if ( J = l , ( I X l ) , .0. ) ) ) )`
28 ringmnd
` |-  ( R e. Ring -> R e. Mnd )`
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> R e. Mnd )`
30 1 2 matrcl
` |-  ( X e. B -> ( N e. Fin /\ R e. _V ) )`
31 30 simpld
` |-  ( X e. B -> N e. Fin )`
` |-  ( ( X e. B /\ C e. V /\ K e. N ) -> N e. Fin )`
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> N e. Fin )`
34 eqcom
` |-  ( J = l <-> l = J )`
35 ifbi
` |-  ( ( J = l <-> l = J ) -> if ( J = l , ( I X l ) , .0. ) = if ( l = J , ( I X l ) , .0. ) )`
36 oveq2
` |-  ( l = J -> ( I X l ) = ( I X J ) )`
` |-  ( ( ( J = l <-> l = J ) /\ l = J ) -> ( I X l ) = ( I X J ) )`
38 37 ifeq1da
` |-  ( ( J = l <-> l = J ) -> if ( l = J , ( I X l ) , .0. ) = if ( l = J , ( I X J ) , .0. ) )`
39 35 38 eqtrd
` |-  ( ( J = l <-> l = J ) -> if ( J = l , ( I X l ) , .0. ) = if ( l = J , ( I X J ) , .0. ) )`
40 34 39 ax-mp
` |-  if ( J = l , ( I X l ) , .0. ) = if ( l = J , ( I X J ) , .0. )`
41 40 mpteq2i
` |-  ( l e. N |-> if ( J = l , ( I X l ) , .0. ) ) = ( l e. N |-> if ( l = J , ( I X J ) , .0. ) )`
42 2 eleq2i
` |-  ( X e. B <-> X e. ( Base ` A ) )`
43 42 biimpi
` |-  ( X e. B -> X e. ( Base ` A ) )`
` |-  ( ( X e. B /\ C e. V /\ K e. N ) -> X e. ( Base ` A ) )`
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> X e. ( Base ` A ) )`
` |-  ( Base ` R ) = ( Base ` R )`
` |-  ( ( I e. N /\ J e. N /\ X e. ( Base ` A ) ) -> ( I X J ) e. ( Base ` R ) )`
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> ( I X J ) e. ( Base ` R ) )`
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> ( R gsum ( l e. N |-> if ( J = l , ( I X l ) , .0. ) ) ) = ( I X J ) )`
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> ( R gsum ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = ( I X J ) )`