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}^{N}$
	ma1repvcl.1	$⊢ \underset{˙}{1} = 1_{A}$
	mulmarep1el.0	$⊢ \underset{˙}{0} = 0_{R}$
	mulmarep1el.e	$⊢ E = (\underset{˙}{1} (N matRepV R) C) (K)$
Assertion	mulmarep1gsum1	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to \underset{l \in N}{\sum_{R}} ((I X l) \cdot_{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}^{N}$
4		ma1repvcl.1	$⊢ \underset{˙}{1} = 1_{A}$
5		mulmarep1el.0	$⊢ \underset{˙}{0} = 0_{R}$
6		mulmarep1el.e	$⊢ E = (\underset{˙}{1} (N matRepV R) C) (K)$
7		simp1	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to R \in Ring$
8	7	adantr	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \land l \in N) \to R \in Ring$
9		simp2	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to (X \in B \land C \in V \land K \in N)$
10	9	adantr	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \land l \in N) \to (X \in B \land C \in V \land K \in N)$
11		simp1	$⊢ (I \in N \land J \in N \land J \neq K) \to I \in N$
12	11	3ad2ant3	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to I \in N$
13	12	adantr	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \land l \in N) \to I \in N$
14		simp2	$⊢ (I \in N \land J \in N \land J \neq K) \to J \in N$
15	14	3ad2ant3	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to J \in N$
16	15	adantr	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \land l \in N) \to J \in N$
17		simpr	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \land l \in N) \to l \in N$
18	1 2 3 4 5 6	mulmarep1el	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land l \in N)) \to (I X l) \cdot_{R} (l E J) = if (J = K, (I X l) \cdot_{R} C (l), if (J = l, I X l, \underset{˙}{0}))$
19	8 10 13 16 17 18	syl113anc	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \land l \in N) \to (I X l) \cdot_{R} (l E J) = if (J = K, (I X l) \cdot_{R} C (l), if (J = l, I X l, \underset{˙}{0}))$
20	19	mpteq2dva	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to (l \in N ⟼ (I X l) \cdot_{R} (l E J)) = (l \in N ⟼ if (J = K, (I X l) \cdot_{R} C (l), if (J = l, I X l, \underset{˙}{0})))$
21	20	oveq2d	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to \underset{l \in N}{\sum_{R}} ((I X l) \cdot_{R} (l E J)) = \underset{l \in N}{\sum_{R}} if (J = K, (I X l) \cdot_{R} C (l), if (J = l, I X l, \underset{˙}{0}))$
22		neneq	$⊢ J \neq K \to \neg J = K$
23	22	3ad2ant3	$⊢ (I \in N \land J \in N \land J \neq K) \to \neg J = K$
24	23	3ad2ant3	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to \neg J = K$
25	24	iffalsed	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to if (J = K, (I X l) \cdot_{R} C (l), if (J = l, I X l, \underset{˙}{0})) = if (J = l, I X l, \underset{˙}{0})$
26	25	mpteq2dv	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to (l \in N ⟼ if (J = K, (I X l) \cdot_{R} C (l), if (J = l, I X l, \underset{˙}{0}))) = (l \in N ⟼ if (J = l, I X l, \underset{˙}{0}))$
27	26	oveq2d	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to \underset{l \in N}{\sum_{R}} if (J = K, (I X l) \cdot_{R} C (l), if (J = l, I X l, \underset{˙}{0})) = \underset{l \in N}{\sum_{R}} if (J = l, I X l, \underset{˙}{0})$
28		ringmnd	$⊢ R \in Ring \to R \in Mnd$
29	28	3ad2ant1	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to R \in Mnd$
30	1 2	matrcl	$⊢ X \in B \to (N \in Fin \land R \in V)$
31	30	simpld	$⊢ X \in B \to N \in Fin$
32	31	3ad2ant1	$⊢ (X \in B \land C \in V \land K \in N) \to N \in Fin$
33	32	3ad2ant2	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to N \in Fin$
34		eqcom	$⊢ J = l \leftrightarrow l = J$
35		ifbi	$⊢ (J = l \leftrightarrow l = J) \to if (J = l, I X l, \underset{˙}{0}) = if (l = J, I X l, \underset{˙}{0})$
36		oveq2	$⊢ l = J \to I X l = I X J$
37	36	adantl	$⊢ ((J = l \leftrightarrow l = J) \land l = J) \to I X l = I X J$
38	37	ifeq1da	$⊢ (J = l \leftrightarrow l = J) \to if (l = J, I X l, \underset{˙}{0}) = if (l = J, I X J, \underset{˙}{0})$
39	35 38	eqtrd	$⊢ (J = l \leftrightarrow l = J) \to if (J = l, I X l, \underset{˙}{0}) = if (l = J, I X J, \underset{˙}{0})$
40	34 39	ax-mp	$⊢ if (J = l, I X l, \underset{˙}{0}) = if (l = J, I X J, \underset{˙}{0})$
41	40	mpteq2i	$⊢ (l \in N ⟼ if (J = l, I X l, \underset{˙}{0})) = (l \in N ⟼ if (l = J, I X J, \underset{˙}{0}))$
42	2	eleq2i	$⊢ X \in B \leftrightarrow X \in {Base}_{A}$
43	42	biimpi	$⊢ X \in B \to X \in {Base}_{A}$
44	43	3ad2ant1	$⊢ (X \in B \land C \in V \land K \in N) \to X \in {Base}_{A}$
45	44	3ad2ant2	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to X \in {Base}_{A}$
46		eqid	$⊢ {Base}_{R} = {Base}_{R}$
47	1 46	matecl	$⊢ (I \in N \land J \in N \land X \in {Base}_{A}) \to I X J \in {Base}_{R}$
48	12 15 45 47	syl3anc	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to I X J \in {Base}_{R}$
49	5 29 33 15 41 48	gsummptif1n0	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to \underset{l \in N}{\sum_{R}} if (J = l, I X l, \underset{˙}{0}) = I X J$
50	21 27 49	3eqtrd	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to \underset{l \in N}{\sum_{R}} ((I X l) \cdot_{R} (l E J)) = I X J$

Metamath Proof Explorer

Theorem mulmarep1gsum1

Proof