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 )
8 7 adantr 
 |-  ( ( ( 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 ) )
10 9 adantr 
 |-  ( ( ( 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 )
12 11 3ad2ant3 
 |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> I e. N )
13 12 adantr 
 |-  ( ( ( 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 )
15 14 3ad2ant3 
 |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> J e. N )
16 15 adantr 
 |-  ( ( ( 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 )
23 22 3ad2ant3 
 |-  ( ( I e. N /\ J e. N /\ J =/= K ) -> -. J = K )
24 23 3ad2ant3 
 |-  ( ( 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 )
29 28 3ad2ant1 
 |-  ( ( 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 )
32 31 3ad2ant1 
 |-  ( ( X e. B /\ C e. V /\ K e. N ) -> N e. Fin )
33 32 3ad2ant2 
 |-  ( ( 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 ) )
37 36 adantl 
 |-  ( ( ( 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 ) )
44 43 3ad2ant1 
 |-  ( ( X e. B /\ C e. V /\ K e. N ) -> X e. ( Base ` A ) )
45 44 3ad2ant2 
 |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> X e. ( Base ` A ) )
46 eqid 
 |-  ( Base ` R ) = ( Base ` R )
47 1 46 matecl 
 |-  ( ( I e. N /\ J e. N /\ X e. ( Base ` A ) ) -> ( I X J ) e. ( Base ` R ) )
48 12 15 45 47 syl3anc 
 |-  ( ( 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 ) )
49 5 29 33 15 41 48 gsummptif1n0 
 |-  ( ( 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 ) )
50 21 27 49 3eqtrd 
 |-  ( ( 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 ) )