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

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 mulmarep1gsum2.x ⊢ × = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
8 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) → 𝑅 ∈ Ring )
9 8 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝑅 ∈ Ring )
10 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ∧ 𝑙 ∈ 𝑁 ) → ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) )
11 simp1 ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) → 𝐼 ∈ 𝑁 )
12 11 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) → 𝐼 ∈ 𝑁 )
13 12 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝐼 ∈ 𝑁 )
14 simpl32 ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝐽 ∈ 𝑁 )
15 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝑙 ∈ 𝑁 )
16 13 14 15 3jca ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ∧ 𝑙 ∈ 𝑁 ) → ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) )
17 9 10 16 3jca ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ∧ 𝑙 ∈ 𝑁 ) → ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ) )
18 17 adantll ⊢ ( ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) ∧ 𝑙 ∈ 𝑁 ) → ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ) )
19 1 2 3 4 5 6 mulmarep1el ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ) → ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) = if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) , if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) )
20 18 19 syl ⊢ ( ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) ∧ 𝑙 ∈ 𝑁 ) → ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) = if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) , if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) )
21 iftrue ⊢ ( 𝐽 = 𝐾 → if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) , if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) = ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) )
22 21 adantr ⊢ ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) → if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) , if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) = ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) )
23 22 adantr ⊢ ( ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) ∧ 𝑙 ∈ 𝑁 ) → if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) , if ( 𝐽 = 𝑙 , ( 𝐼 𝑋 𝑙 ) , 0 ) ) = ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) )
24 20 23 eqtrd ⊢ ( ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) ∧ 𝑙 ∈ 𝑁 ) → ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) = ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) )
25 24 mpteq2dva ⊢ ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) → ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) ) = ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) ) )
26 25 oveq2d ⊢ ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) ) ) = ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) ) ) )
27 fveq1 ⊢ ( ( 𝑋 × 𝐶 ) = 𝑍 → ( ( 𝑋 × 𝐶 ) ‘ 𝐼 ) = ( 𝑍 ‘ 𝐼 ) )
28 27 eqcomd ⊢ ( ( 𝑋 × 𝐶 ) = 𝑍 → ( 𝑍 ‘ 𝐼 ) = ( ( 𝑋 × 𝐶 ) ‘ 𝐼 ) )
29 28 3ad2ant3 ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) → ( 𝑍 ‘ 𝐼 ) = ( ( 𝑋 × 𝐶 ) ‘ 𝐼 ) )
30 29 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) → ( 𝑍 ‘ 𝐼 ) = ( ( 𝑋 × 𝐶 ) ‘ 𝐼 ) )
31 30 adantl ⊢ ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) → ( 𝑍 ‘ 𝐼 ) = ( ( 𝑋 × 𝐶 ) ‘ 𝐼 ) )
32 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
33 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
34 8 adantl ⊢ ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) → 𝑅 ∈ Ring )
35 1 2 matrcl ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
36 35 simpld ⊢ ( 𝑋 ∈ 𝐵 → 𝑁 ∈ Fin )
37 36 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝑁 ∈ Fin )
38 37 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) → 𝑁 ∈ Fin )
39 38 adantl ⊢ ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) → 𝑁 ∈ Fin )
40 2 eleq2i ⊢ ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ( Base ‘ 𝐴 ) )
41 40 biimpi ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
42 41 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
43 42 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
44 43 adantl ⊢ ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
45 3 eleq2i ⊢ ( 𝐶 ∈ 𝑉 ↔ 𝐶 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
46 45 biimpi ⊢ ( 𝐶 ∈ 𝑉 → 𝐶 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
47 46 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝐶 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
48 47 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) → 𝐶 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
49 48 adantl ⊢ ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) → 𝐶 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
50 12 adantl ⊢ ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) → 𝐼 ∈ 𝑁 )
51 1 7 32 33 34 39 44 49 50 mavmulfv ⊢ ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) → ( ( 𝑋 × 𝐶 ) ‘ 𝐼 ) = ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) ) ) )
52 31 51 eqtrd ⊢ ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) → ( 𝑍 ‘ 𝐼 ) = ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝑙 ) ) ) ) )
53 iftrue ⊢ ( 𝐽 = 𝐾 → if ( 𝐽 = 𝐾 , ( 𝑍 ‘ 𝐼 ) , ( 𝐼 𝑋 𝐽 ) ) = ( 𝑍 ‘ 𝐼 ) )
54 53 eqcomd ⊢ ( 𝐽 = 𝐾 → ( 𝑍 ‘ 𝐼 ) = if ( 𝐽 = 𝐾 , ( 𝑍 ‘ 𝐼 ) , ( 𝐼 𝑋 𝐽 ) ) )
55 54 adantr ⊢ ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) → ( 𝑍 ‘ 𝐼 ) = if ( 𝐽 = 𝐾 , ( 𝑍 ‘ 𝐼 ) , ( 𝐼 𝑋 𝐽 ) ) )
56 26 52 55 3eqtr2d ⊢ ( ( 𝐽 = 𝐾 ∧ ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) ) ) = if ( 𝐽 = 𝐾 , ( 𝑍 ‘ 𝐼 ) , ( 𝐼 𝑋 𝐽 ) ) )
57 56 ex ⊢ ( 𝐽 = 𝐾 → ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) ) ) = if ( 𝐽 = 𝐾 , ( 𝑍 ‘ 𝐼 ) , ( 𝐼 𝑋 𝐽 ) ) ) )
58 8 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ∧ 𝐽 ≠ 𝐾 ) → 𝑅 ∈ Ring )
59 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ∧ 𝐽 ≠ 𝐾 ) → ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) )
60 12 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ∧ 𝐽 ≠ 𝐾 ) → 𝐼 ∈ 𝑁 )
61 simpl32 ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ∧ 𝐽 ≠ 𝐾 ) → 𝐽 ∈ 𝑁 )
62 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ∧ 𝐽 ≠ 𝐾 ) → 𝐽 ≠ 𝐾 )
63 1 2 3 4 5 6 mulmarep1gsum1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾 ) ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) ) ) = ( 𝐼 𝑋 𝐽 ) )
64 58 59 60 61 62 63 syl113anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ∧ 𝐽 ≠ 𝐾 ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) ) ) = ( 𝐼 𝑋 𝐽 ) )
65 df-ne ⊢ ( 𝐽 ≠ 𝐾 ↔ ¬ 𝐽 = 𝐾 )
66 iffalse ⊢ ( ¬ 𝐽 = 𝐾 → if ( 𝐽 = 𝐾 , ( 𝑍 ‘ 𝐼 ) , ( 𝐼 𝑋 𝐽 ) ) = ( 𝐼 𝑋 𝐽 ) )
67 66 eqcomd ⊢ ( ¬ 𝐽 = 𝐾 → ( 𝐼 𝑋 𝐽 ) = if ( 𝐽 = 𝐾 , ( 𝑍 ‘ 𝐼 ) , ( 𝐼 𝑋 𝐽 ) ) )
68 65 67 sylbi ⊢ ( 𝐽 ≠ 𝐾 → ( 𝐼 𝑋 𝐽 ) = if ( 𝐽 = 𝐾 , ( 𝑍 ‘ 𝐼 ) , ( 𝐼 𝑋 𝐽 ) ) )
69 68 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ∧ 𝐽 ≠ 𝐾 ) → ( 𝐼 𝑋 𝐽 ) = if ( 𝐽 = 𝐾 , ( 𝑍 ‘ 𝐼 ) , ( 𝐼 𝑋 𝐽 ) ) )
70 64 69 eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) ∧ 𝐽 ≠ 𝐾 ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) ) ) = if ( 𝐽 = 𝐾 , ( 𝑍 ‘ 𝐼 ) , ( 𝐼 𝑋 𝐽 ) ) )
71 70 expcom ⊢ ( 𝐽 ≠ 𝐾 → ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) ) ) = if ( 𝐽 = 𝐾 , ( 𝑍 ‘ 𝐼 ) , ( 𝐼 𝑋 𝐽 ) ) ) )
72 57 71 pm2.61ine ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ ( 𝑋 × 𝐶 ) = 𝑍 ) ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝐽 ) ) ) ) = if ( 𝐽 = 𝐾 , ( 𝑍 ‘ 𝐼 ) , ( 𝐼 𝑋 𝐽 ) ) )