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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	marepvcl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	marepvcl.v	⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
	ma1repvcl.1	⊢ 1 = ( 1r ‘ 𝐴 )
	mulmarep1el.0	⊢ 0 = ( 0g ‘ 𝑅 )
	mulmarep1el.e	⊢ 𝐸 = ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝐶 ) ‘ 𝐾 )
Assertion	mulmarep1gsum1	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) ) ) = ( 𝐼 𝑋 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		marepvcl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		marepvcl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		marepvcl.v	⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
4		ma1repvcl.1	⊢ 1 = ( 1r ‘ 𝐴 )
5		mulmarep1el.0	⊢ 0 = ( 0g ‘ 𝑅 )
6		mulmarep1el.e	⊢ 𝐸 = ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝐶 ) ‘ 𝐾 )
7		simp1	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → 𝑅 ∈ Ring )
8	7	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝑅 ∈ Ring )
9		simp2	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) )
10	9	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) ∧ 𝑙 ∈ 𝑁 ) → ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) )
11		simp1	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) → 𝐼 ∈ 𝑁 )
12	11	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → 𝐼 ∈ 𝑁 )
13	12	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝐼 ∈ 𝑁 )
14		simp2	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) → 𝐽 ∈ 𝑁 )
15	14	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → 𝐽 ∈ 𝑁 )
16	15	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝐽 ∈ 𝑁 )
17		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝑙 ∈ 𝑁 )
18	1 2 3 4 5 6	mulmarep1el	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ) → ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) = if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) , if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) )
19	8 10 13 16 17 18	syl113anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) ∧ 𝑙 ∈ 𝑁 ) → ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) = if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) , if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) )
20	19	mpteq2dva	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) ) = ( 𝑙 ∈ 𝑁 ↦ if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) , if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) ) )
21	20	oveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) ) ) = ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) , if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) ) ) )
22		neneq	⊢ ( 𝐽 ≠ 𝐾 → ¬ 𝐽 = 𝐾 )
23	22	3ad2ant3	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) → ¬ 𝐽 = 𝐾 )
24	23	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → ¬ 𝐽 = 𝐾 )
25	24	iffalsed	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) , if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) = if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) )
26	25	mpteq2dv	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → ( 𝑙 ∈ 𝑁 ↦ if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) , if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) ) = ( 𝑙 ∈ 𝑁 ↦ if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) )
27	26	oveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) , if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) ) ) = ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) ) )
28		ringmnd	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
29	28	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → 𝑅 ∈ Mnd )
30	1 2	matrcl	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
31	30	simpld	⊢ ( 𝑋 ∈ 𝐵 → 𝑁 ∈ Fin )
32	31	3ad2ant1	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝑁 ∈ Fin )
33	32	3ad2ant2	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → 𝑁 ∈ Fin )
34		eqcom	⊢ ( 𝐽 = 𝑙 ↔ 𝑙 = 𝐽 )
35		ifbi	⊢ ( ( 𝐽 = 𝑙 ↔ 𝑙 = 𝐽 ) → if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) = if ( 𝑙 = 𝐽 , ( 𝐼 𝑋 𝑙 ) , 0 ) )
36		oveq2	⊢ ( 𝑙 = 𝐽 → ( 𝐼 𝑋 𝑙 ) = ( 𝐼 𝑋 𝐽 ) )
37	36	adantl	⊢ ( ( ( 𝐽 = 𝑙 ↔ 𝑙 = 𝐽 ) ∧ 𝑙 = 𝐽 ) → ( 𝐼 𝑋 𝑙 ) = ( 𝐼 𝑋 𝐽 ) )
38	37	ifeq1da	⊢ ( ( 𝐽 = 𝑙 ↔ 𝑙 = 𝐽 ) → if ( 𝑙 = 𝐽 , ( 𝐼 𝑋 𝑙 ) , 0 ) = if ( 𝑙 = 𝐽 , ( 𝐼 𝑋 𝐽 ) , 0 ) )
39	35 38	eqtrd	⊢ ( ( 𝐽 = 𝑙 ↔ 𝑙 = 𝐽 ) → if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) = if ( 𝑙 = 𝐽 , ( 𝐼 𝑋 𝐽 ) , 0 ) )
40	34 39	ax-mp	⊢ if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) = if ( 𝑙 = 𝐽 , ( 𝐼 𝑋 𝐽 ) , 0 )
41	40	mpteq2i	⊢ ( 𝑙 ∈ 𝑁 ↦ if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) = ( 𝑙 ∈ 𝑁 ↦ if ( 𝑙 = 𝐽 , ( 𝐼 𝑋 𝐽 ) , 0 ) )
42	2	eleq2i	⊢ ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ( Base ‘ 𝐴 ) )
43	42	biimpi	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
44	43	3ad2ant1	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
45	44	3ad2ant2	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
46		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
47	1 46	matecl	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) → ( 𝐼 𝑋 𝐽 ) ∈ ( Base ‘ 𝑅 ) )
48	12 15 45 47	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → ( 𝐼 𝑋 𝐽 ) ∈ ( Base ‘ 𝑅 ) )
49	5 29 33 15 41 48	gsummptif1n0	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) ) = ( 𝐼 𝑋 𝐽 ) )
50	21 27 49	3eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) ) ) = ( 𝐼 𝑋 𝐽 ) )