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	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	chpdmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	chpdmat.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
	chpdmat.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	chpdmat.x	⊢ 𝑋 = ( var₁ ‘ 𝑅 )
	chpdmat.0	⊢ 0 = ( 0_g ‘ 𝑅 )
	chpdmat.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
	chpdmat.m	⊢ − = ( -_g ‘ 𝑃 )
Assertion	chpdmat	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝐶 ‘ 𝑀 ) = ( 𝐺 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 − ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		chpdmat.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2		chpdmat.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
3		chpdmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		chpdmat.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
5		chpdmat.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
6		chpdmat.x	⊢ 𝑋 = ( var₁ ‘ 𝑅 )
7		chpdmat.0	⊢ 0 = ( 0_g ‘ 𝑅 )
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	⊢ ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) = ( 1_r ‘ ( 𝑁 Mat 𝑃 ) )
16	1 3 5 2 10 11 12 6 13 14 15	chpmatval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) = ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ) )
17	16	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝐶 ‘ 𝑀 ) = ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 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 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
24	22 23	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
25	19 20 24	3jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑃 ∈ CRing ∧ 𝑁 ∈ Fin ∧ ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) ) )
26	25	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝑃 ∈ CRing ∧ 𝑁 ∈ Fin ∧ ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 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 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0_g ‘ 𝑃 ) )
30	28 29	sylanl1	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑖 ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0_g ‘ 𝑃 ) )
31	30	exp31	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ≠ 𝑗 → ( ( 𝑖 𝑀 𝑗 ) = 0 → ( 𝑖 ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0_g ‘ 𝑃 ) ) ) )
32	31	a2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑖 ≠ 𝑗 → ( 𝑖 ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0_g ‘ 𝑃 ) ) ) )
33	32	ralimdva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) → ( ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) → ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0_g ‘ 𝑃 ) ) ) )
34	33	ralimdva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0_g ‘ 𝑃 ) ) ) )
35	34	imp	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0_g ‘ 𝑃 ) ) )
36		eqid	⊢ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) = ( Base ‘ ( 𝑁 Mat 𝑃 ) )
37		eqid	⊢ ( 0_g ‘ 𝑃 ) = ( 0_g ‘ 𝑃 )
38	11 10 36 8 37	mdetdiag	⊢ ( ( 𝑃 ∈ CRing ∧ 𝑁 ∈ Fin ∧ ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑗 ) = ( 0_g ‘ 𝑃 ) ) → ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ) = ( 𝐺 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑘 ) ) ) ) )
39	26 35 38	sylc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ) = ( 𝐺 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑘 ) ) ) )
40	1 2 3 4 5 6 7 8 9 10 15 13 12 14	chpdmatlem3	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑘 ) = ( 𝑋 − ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) )
41	22 40	sylan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑘 ) = ( 𝑋 − ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) )
42	41	adantlr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑘 ) = ( 𝑋 − ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) )
43	42	mpteq2dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑘 ) ) = ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 − ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) ) )
44	43	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝐺 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 ( ( 𝑋 ( ·_𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1_r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -_g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝑘 ) ) ) = ( 𝐺 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 − ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) ) ) )
45	17 39 44	3eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝐶 ‘ 𝑀 ) = ( 𝐺 Σ_g ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 − ( 𝑆 ‘ ( 𝑘 𝑀 𝑘 ) ) ) ) ) )

Metamath Proof Explorer

Theorem chpdmat

Proof