Metamath Proof Explorer

Theorem chpdmat

Description: The characteristic polynomial of a diagonal matrix. (Contributed by AV, 18-Aug-2019) (Proof shortened by AV, 21-Nov-2019)

Ref Expression
Hypotheses chpdmat.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
chpdmat.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
chpdmat.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
chpdmat.s ⊢ 𝑆 = ( algSc ‘ 𝑃 )
chpdmat.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
chpdmat.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
chpdmat.0 ⊢ 0 = ( 0g ‘ 𝑅 )
chpdmat.g ⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
chpdmat.m ⊢ − = ( -g ‘ 𝑃 )
Assertion chpdmat ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝐶 ‘ 𝑀 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 − ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 chpdmat.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2 chpdmat.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 chpdmat.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4 chpdmat.s ⊢ 𝑆 = ( algSc ‘ 𝑃 )
5 chpdmat.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
6 chpdmat.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
7 chpdmat.0 ⊢ 0 = ( 0g ‘ 𝑅 )
8 chpdmat.g ⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
9 chpdmat.m ⊢ − = ( -g ‘ 𝑃 )
10 eqid ⊢ ( 𝑁 Mat 𝑃 ) = ( 𝑁 Mat 𝑃 )
11 eqid ⊢ ( 𝑁 maDet 𝑃 ) = ( 𝑁 maDet 𝑃 )
12 eqid ⊢ ( -g ‘ ( 𝑁 Mat 𝑃 ) ) = ( -g ‘ ( 𝑁 Mat 𝑃 ) )
13 eqid ⊢ ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) = ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) )
14 eqid ⊢ ( 𝑁 matToPolyMat 𝑅 ) = ( 𝑁 matToPolyMat 𝑅 )
15 eqid ⊢ ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) = ( 1r ‘ ( 𝑁 Mat 𝑃 ) )
16 1 3 5 2 10 11 12 6 13 14 15 chpmatval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) = ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ) )
17 16 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝐶 ‘ 𝑀 ) = ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ) )
18 2 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
19 18 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ CRing )
20 simp1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ Fin )
21 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
22 21 3anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) )
23 1 2 3 4 5 6 7 8 9 10 15 13 12 14 chpdmatlem1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
24 22 23 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
25 19 20 24 3jca ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑃 ∈ CRing ∧ 𝑁 ∈ Fin ∧ ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) ) )
26 25 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝑃 ∈ CRing ∧ 𝑁 ∈ Fin ∧ ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) ) )
27 22 anim1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) )
28 27 anim1i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) )
29 1 2 3 4 5 6 7 8 9 10 15 13 12 14 chpdmatlem2 ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑖 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0g ‘ 𝑃 ) )
30 28 29 sylanl1 ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑖 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0g ‘ 𝑃 ) )
31 30 exp31 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ≠ 𝑗 → ( ( 𝑖 𝑀 𝑗 ) = 0 → ( 𝑖 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0g ‘ 𝑃 ) ) ) )
32 31 a2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑖 ≠ 𝑗 → ( 𝑖 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0g ‘ 𝑃 ) ) ) )
33 32 ralimdva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) → ( ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) → ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0g ‘ 𝑃 ) ) ) )
34 33 ralimdva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0g ‘ 𝑃 ) ) ) )
35 34 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0g ‘ 𝑃 ) ) )
36 eqid ⊢ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) = ( Base ‘ ( 𝑁 Mat 𝑃 ) )
37 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
38 11 10 36 8 37 mdetdiag ⊢ ( ( 𝑃 ∈ CRing ∧ 𝑁 ∈ Fin ∧ ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0g ‘ 𝑃 ) ) → ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑘 ) ) ) ) )
39 26 35 38 sylc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑘 ) ) ) )
40 1 2 3 4 5 6 7 8 9 10 15 13 12 14 chpdmatlem3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑘 ) = ( 𝑋 − ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) )
41 22 40 sylan ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑘 ) = ( 𝑋 − ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) )
42 41 adantlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑘 ) = ( 𝑋 − ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) )
43 42 mpteq2dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑘 ) ) = ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 − ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) ) )
44 43 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑘 ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 − ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) ) ) )
45 17 39 44 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝐶 ‘ 𝑀 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 − ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) ) ) )