# 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}\mathrm{Mat}{R}$
marepvcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
marepvcl.v ${⊢}{V}={{\mathrm{Base}}_{{R}}}^{{N}}$
ma1repvcl.1
mulmarep1el.0
mulmarep1el.e
Assertion mulmarep1gsum1 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\to \underset{{l}\in {N}}{{\sum }_{{R}}}\left(\left({I}{X}{l}\right){\cdot }_{{R}}\left({l}{E}{J}\right)\right)={I}{X}{J}$

### Proof

Step Hyp Ref Expression
1 marepvcl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 marepvcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 marepvcl.v ${⊢}{V}={{\mathrm{Base}}_{{R}}}^{{N}}$
4 ma1repvcl.1
5 mulmarep1el.0
6 mulmarep1el.e
7 simp1 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\to {R}\in \mathrm{Ring}$
8 7 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\wedge {l}\in {N}\right)\to {R}\in \mathrm{Ring}$
9 simp2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\to \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)$
10 9 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\wedge {l}\in {N}\right)\to \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)$
11 simp1 ${⊢}\left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\to {I}\in {N}$
12 11 3ad2ant3 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\to {I}\in {N}$
13 12 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\wedge {l}\in {N}\right)\to {I}\in {N}$
14 simp2 ${⊢}\left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\to {J}\in {N}$
15 14 3ad2ant3 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\to {J}\in {N}$
16 15 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\wedge {l}\in {N}\right)\to {J}\in {N}$
17 simpr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\wedge {l}\in {N}\right)\to {l}\in {N}$
18 1 2 3 4 5 6 mulmarep1el
19 8 10 13 16 17 18 syl113anc
20 19 mpteq2dva
21 20 oveq2d
22 neneq ${⊢}{J}\ne {K}\to ¬{J}={K}$
23 22 3ad2ant3 ${⊢}\left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\to ¬{J}={K}$
24 23 3ad2ant3 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\to ¬{J}={K}$
25 24 iffalsed
26 25 mpteq2dv
27 26 oveq2d
28 ringmnd ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Mnd}$
29 28 3ad2ant1 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\to {R}\in \mathrm{Mnd}$
30 1 2 matrcl ${⊢}{X}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
31 30 simpld ${⊢}{X}\in {B}\to {N}\in \mathrm{Fin}$
32 31 3ad2ant1 ${⊢}\left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\to {N}\in \mathrm{Fin}$
33 32 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\to {N}\in \mathrm{Fin}$
34 eqcom ${⊢}{J}={l}↔{l}={J}$
35 ifbi
36 oveq2 ${⊢}{l}={J}\to {I}{X}{l}={I}{X}{J}$
37 36 adantl ${⊢}\left(\left({J}={l}↔{l}={J}\right)\wedge {l}={J}\right)\to {I}{X}{l}={I}{X}{J}$
38 37 ifeq1da
39 35 38 eqtrd
40 34 39 ax-mp
41 40 mpteq2i
42 2 eleq2i ${⊢}{X}\in {B}↔{X}\in {\mathrm{Base}}_{{A}}$
43 42 biimpi ${⊢}{X}\in {B}\to {X}\in {\mathrm{Base}}_{{A}}$
44 43 3ad2ant1 ${⊢}\left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\to {X}\in {\mathrm{Base}}_{{A}}$
45 44 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\to {X}\in {\mathrm{Base}}_{{A}}$
46 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
47 1 46 matecl ${⊢}\left({I}\in {N}\wedge {J}\in {N}\wedge {X}\in {\mathrm{Base}}_{{A}}\right)\to {I}{X}{J}\in {\mathrm{Base}}_{{R}}$
48 12 15 45 47 syl3anc ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\to {I}{X}{J}\in {\mathrm{Base}}_{{R}}$
49 5 29 33 15 41 48 gsummptif1n0
50 21 27 49 3eqtrd ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {J}\ne {K}\right)\right)\to \underset{{l}\in {N}}{{\sum }_{{R}}}\left(\left({I}{X}{l}\right){\cdot }_{{R}}\left({l}{E}{J}\right)\right)={I}{X}{J}$