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}\mathrm{Mat}{R}$
marepvcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
marepvcl.v ${⊢}{V}={{\mathrm{Base}}_{{R}}}^{{N}}$
ma1repvcl.1
mulmarep1el.0
mulmarep1el.e
mulmarep1gsum2.x
Assertion mulmarep1gsum2

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