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 )
18 17 3ad2ant3
 |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> I e. N )
19 7 3ad2ant3
 |-  ( ( 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 ) )
22 21 3ad2ant1
 |-  ( ( X e. B /\ C e. V /\ K e. N ) -> X e. ( Base ` A ) )
23 22 3ad2ant2
 |-  ( ( 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 eqtrid
 |-  ( ( 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. ) ) )