Metamath Proof Explorer

Theorem mulmarep1gsum2

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, 18-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 )
mulmarep1gsum2.x 
|- .X. = ( R maVecMul <. N , N >. )
Assertion mulmarep1gsum2 
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> ( R gsum ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = if ( J = K , ( Z ` I ) , ( 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 mulmarep1gsum2.x 
 |-  .X. = ( R maVecMul <. N , N >. )
8 simp1 
 |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> R e. Ring )
9 8 adantr 
 |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ l e. N ) -> R e. Ring )
10 simpl2 
 |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ l e. N ) -> ( X e. B /\ C e. V /\ K e. N ) )
11 simp1 
 |-  ( ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) -> I e. N )
12 11 3ad2ant3 
 |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> I e. N )
13 12 adantr 
 |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ l e. N ) -> I e. N )
14 simpl32 
 |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ l e. N ) -> J e. N )
15 simpr 
 |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ l e. N ) -> l e. N )
16 13 14 15 3jca 
 |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ l e. N ) -> ( I e. N /\ J e. N /\ l e. N ) )
17 9 10 16 3jca 
 |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ l e. N ) -> ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ l e. N ) ) )
18 17 adantll 
 |-  ( ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) /\ l e. N ) -> ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ l e. N ) ) )
19 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. ) ) )
20 18 19 syl 
 |-  ( ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) /\ 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. ) ) )
21 iftrue 
 |-  ( J = K -> if ( J = K , ( ( I X l ) ( .r ` R ) ( C ` l ) ) , if ( J = l , ( I X l ) , .0. ) ) = ( ( I X l ) ( .r ` R ) ( C ` l ) ) )
22 21 adantr 
 |-  ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> if ( J = K , ( ( I X l ) ( .r ` R ) ( C ` l ) ) , if ( J = l , ( I X l ) , .0. ) ) = ( ( I X l ) ( .r ` R ) ( C ` l ) ) )
23 22 adantr 
 |-  ( ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) /\ l e. N ) -> if ( J = K , ( ( I X l ) ( .r ` R ) ( C ` l ) ) , if ( J = l , ( I X l ) , .0. ) ) = ( ( I X l ) ( .r ` R ) ( C ` l ) ) )
24 20 23 eqtrd 
 |-  ( ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) /\ l e. N ) -> ( ( I X l ) ( .r ` R ) ( l E J ) ) = ( ( I X l ) ( .r ` R ) ( C ` l ) ) )
25 24 mpteq2dva 
 |-  ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) = ( l e. N |-> ( ( I X l ) ( .r ` R ) ( C ` l ) ) ) )
26 25 oveq2d 
 |-  ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> ( R gsum ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = ( R gsum ( l e. N |-> ( ( I X l ) ( .r ` R ) ( C ` l ) ) ) ) )
27 fveq1 
 |-  ( ( X .X. C ) = Z -> ( ( X .X. C ) ` I ) = ( Z ` I ) )
28 27 eqcomd 
 |-  ( ( X .X. C ) = Z -> ( Z ` I ) = ( ( X .X. C ) ` I ) )
29 28 3ad2ant3 
 |-  ( ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) -> ( Z ` I ) = ( ( X .X. C ) ` I ) )
30 29 3ad2ant3 
 |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> ( Z ` I ) = ( ( X .X. C ) ` I ) )
31 30 adantl 
 |-  ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> ( Z ` I ) = ( ( X .X. C ) ` I ) )
32 eqid 
 |-  ( Base ` R ) = ( Base ` R )
33 eqid 
 |-  ( .r ` R ) = ( .r ` R )
34 8 adantl 
 |-  ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> R e. Ring )
35 1 2 matrcl 
 |-  ( X e. B -> ( N e. Fin /\ R e. _V ) )
36 35 simpld 
 |-  ( X e. B -> N e. Fin )
37 36 3ad2ant1 
 |-  ( ( X e. B /\ C e. V /\ K e. N ) -> N e. Fin )
38 37 3ad2ant2 
 |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> N e. Fin )
39 38 adantl 
 |-  ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> N e. Fin )
40 2 eleq2i 
 |-  ( X e. B <-> X e. ( Base ` A ) )
41 40 biimpi 
 |-  ( X e. B -> X e. ( Base ` A ) )
42 41 3ad2ant1 
 |-  ( ( X e. B /\ C e. V /\ K e. N ) -> X e. ( Base ` A ) )
43 42 3ad2ant2 
 |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> X e. ( Base ` A ) )
44 43 adantl 
 |-  ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> X e. ( Base ` A ) )
45 3 eleq2i 
 |-  ( C e. V <-> C e. ( ( Base ` R ) ^m N ) )
46 45 biimpi 
 |-  ( C e. V -> C e. ( ( Base ` R ) ^m N ) )
47 46 3ad2ant2 
 |-  ( ( X e. B /\ C e. V /\ K e. N ) -> C e. ( ( Base ` R ) ^m N ) )
48 47 3ad2ant2 
 |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> C e. ( ( Base ` R ) ^m N ) )
49 48 adantl 
 |-  ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> C e. ( ( Base ` R ) ^m N ) )
50 12 adantl 
 |-  ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> I e. N )
51 1 7 32 33 34 39 44 49 50 mavmulfv 
 |-  ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> ( ( X .X. C ) ` I ) = ( R gsum ( l e. N |-> ( ( I X l ) ( .r ` R ) ( C ` l ) ) ) ) )
52 31 51 eqtrd 
 |-  ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> ( Z ` I ) = ( R gsum ( l e. N |-> ( ( I X l ) ( .r ` R ) ( C ` l ) ) ) ) )
53 iftrue 
 |-  ( J = K -> if ( J = K , ( Z ` I ) , ( I X J ) ) = ( Z ` I ) )
54 53 eqcomd 
 |-  ( J = K -> ( Z ` I ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )
55 54 adantr 
 |-  ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> ( Z ` I ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )
56 26 52 55 3eqtr2d 
 |-  ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> ( R gsum ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )
57 56 ex 
 |-  ( J = K -> ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> ( R gsum ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = if ( J = K , ( Z ` I ) , ( I X J ) ) ) )
58 8 adantr 
 |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> R e. Ring )
59 simpl2 
 |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> ( X e. B /\ C e. V /\ K e. N ) )
60 12 adantr 
 |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> I e. N )
61 simpl32 
 |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> J e. N )
62 simpr 
 |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> J =/= K )
63 1 2 3 4 5 6 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 ) )
64 58 59 60 61 62 63 syl113anc 
 |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> ( R gsum ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = ( I X J ) )
65 df-ne 
 |-  ( J =/= K <-> -. J = K )
66 iffalse 
 |-  ( -. J = K -> if ( J = K , ( Z ` I ) , ( I X J ) ) = ( I X J ) )
67 66 eqcomd 
 |-  ( -. J = K -> ( I X J ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )
68 65 67 sylbi 
 |-  ( J =/= K -> ( I X J ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )
69 68 adantl 
 |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> ( I X J ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )
70 64 69 eqtrd 
 |-  ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> ( R gsum ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )
71 70 expcom 
 |-  ( J =/= K -> ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> ( R gsum ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = if ( J = K , ( Z ` I ) , ( I X J ) ) ) )
72 57 71 pm2.61ine 
 |-  ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> ( R gsum ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )