This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 = ( 𝑁 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 ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) ) ) = ( 𝐼 𝑋 𝐽 ) )