# Metamath Proof Explorer

## Theorem mulmarep1el

Description: Element by element multiplication 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 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. ) ) )`

### 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 simp3
` |-  ( ( I e. N /\ J e. N /\ L e. N ) -> L e. N )`
8 simp2
` |-  ( ( I e. N /\ J e. N /\ L e. N ) -> J e. N )`
9 7 8 jca
` |-  ( ( I e. N /\ J e. N /\ L e. N ) -> ( L e. N /\ J e. N ) )`
10 1 2 3 4 5 6 ma1repveval
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( L e. N /\ J e. N ) ) -> ( L E J ) = if ( J = K , ( C ` L ) , if ( J = L , ( 1r ` R ) , .0. ) ) )`
11 9 10 syl3an3
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> ( L E J ) = if ( J = K , ( C ` L ) , if ( J = L , ( 1r ` R ) , .0. ) ) )`
12 11 oveq2d
` |-  ( ( 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 ) ) = ( ( I X L ) ( .r ` R ) if ( J = K , ( C ` L ) , if ( J = L , ( 1r ` R ) , .0. ) ) ) )`
13 ovif2
` |-  ( ( I X L ) ( .r ` R ) if ( J = K , ( C ` L ) , if ( J = L , ( 1r ` R ) , .0. ) ) ) = if ( J = K , ( ( I X L ) ( .r ` R ) ( C ` L ) ) , ( ( I X L ) ( .r ` R ) if ( J = L , ( 1r ` R ) , .0. ) ) )`
14 13 a1i
` |-  ( ( 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 ) if ( J = K , ( C ` L ) , if ( J = L , ( 1r ` R ) , .0. ) ) ) = if ( J = K , ( ( I X L ) ( .r ` R ) ( C ` L ) ) , ( ( I X L ) ( .r ` R ) if ( J = L , ( 1r ` R ) , .0. ) ) ) )`
15 ovif2
` |-  ( ( I X L ) ( .r ` R ) if ( J = L , ( 1r ` R ) , .0. ) ) = if ( J = L , ( ( I X L ) ( .r ` R ) ( 1r ` R ) ) , ( ( I X L ) ( .r ` R ) .0. ) )`
16 simp1
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> R e. Ring )`
17 simp1
` |-  ( ( I e. N /\ J e. N /\ L e. N ) -> I e. N )`
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> I e. N )`
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> L e. N )`
20 2 eleq2i
` |-  ( X e. B <-> X e. ( Base ` A ) )`
21 20 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 /\ L e. N ) ) -> X e. ( Base ` A ) )`
24 eqid
` |-  ( Base ` R ) = ( Base ` R )`
25 1 24 matecl
` |-  ( ( I e. N /\ L e. N /\ X e. ( Base ` A ) ) -> ( I X L ) e. ( Base ` R ) )`
26 18 19 23 25 syl3anc
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> ( I X L ) e. ( Base ` R ) )`
27 eqid
` |-  ( .r ` R ) = ( .r ` R )`
28 eqid
` |-  ( 1r ` R ) = ( 1r ` R )`
29 24 27 28 ringridm
` |-  ( ( R e. Ring /\ ( I X L ) e. ( Base ` R ) ) -> ( ( I X L ) ( .r ` R ) ( 1r ` R ) ) = ( I X L ) )`
30 16 26 29 syl2anc
` |-  ( ( 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 ) ( 1r ` R ) ) = ( I X L ) )`
31 24 27 5 ringrz
` |-  ( ( R e. Ring /\ ( I X L ) e. ( Base ` R ) ) -> ( ( I X L ) ( .r ` R ) .0. ) = .0. )`
32 16 26 31 syl2anc
` |-  ( ( 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 ) .0. ) = .0. )`
33 30 32 ifeq12d
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> if ( J = L , ( ( I X L ) ( .r ` R ) ( 1r ` R ) ) , ( ( I X L ) ( .r ` R ) .0. ) ) = if ( J = L , ( I X L ) , .0. ) )`
34 15 33 syl5eq
` |-  ( ( 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 ) if ( J = L , ( 1r ` R ) , .0. ) ) = if ( J = L , ( I X L ) , .0. ) )`
35 34 ifeq2d
` |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> if ( J = K , ( ( I X L ) ( .r ` R ) ( C ` L ) ) , ( ( I X L ) ( .r ` R ) if ( J = L , ( 1r ` R ) , .0. ) ) ) = if ( J = K , ( ( I X L ) ( .r ` R ) ( C ` L ) ) , if ( J = L , ( I X L ) , .0. ) ) )`
36 12 14 35 3eqtrd
` |-  ( ( 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. ) ) )`