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 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. ) ) )