Theorem cayleyhamilton0

Description: The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation". This version of cayleyhamilton provides definitions not used in the theorem itself, but in its proof to make it clearer, more readable and shorter compared with a proof without them (see cayleyhamiltonALT )! (Contributed by AV, 25-Nov-2019) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	cayleyhamilton0.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	cayleyhamilton0.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	cayleyhamilton0.0	⊢ 0 = ( 0g ‘ 𝐴 )
	cayleyhamilton0.1	⊢ 1 = ( 1r ‘ 𝐴 )
	cayleyhamilton0.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
	cayleyhamilton0.e1	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐴 ) )
	cayleyhamilton0.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	cayleyhamilton0.k	⊢ 𝐾 = ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) )
	cayleyhamilton0.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	cayleyhamilton0.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
	cayleyhamilton0.r	⊢ × = ( .r ‘ 𝑌 )
	cayleyhamilton0.s	⊢ − = ( -g ‘ 𝑌 )
	cayleyhamilton0.z	⊢ 𝑍 = ( 0g ‘ 𝑌 )
	cayleyhamilton0.w	⊢ 𝑊 = ( Base ‘ 𝑌 )
	cayleyhamilton0.e2	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑌 ) )
	cayleyhamilton0.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	cayleyhamilton0.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 𝑍 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 𝑍 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
	cayleyhamilton0.u	⊢ 𝑈 = ( 𝑁 cPolyMatToMat 𝑅 )
Assertion	cayleyhamilton0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		cayleyhamilton0.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		cayleyhamilton0.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		cayleyhamilton0.0	⊢ 0 = ( 0g ‘ 𝐴 )
4		cayleyhamilton0.1	⊢ 1 = ( 1r ‘ 𝐴 )
5		cayleyhamilton0.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
6		cayleyhamilton0.e1	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐴 ) )
7		cayleyhamilton0.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
8		cayleyhamilton0.k	⊢ 𝐾 = ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) )
9		cayleyhamilton0.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
10		cayleyhamilton0.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
11		cayleyhamilton0.r	⊢ × = ( .r ‘ 𝑌 )
12		cayleyhamilton0.s	⊢ − = ( -g ‘ 𝑌 )
13		cayleyhamilton0.z	⊢ 𝑍 = ( 0g ‘ 𝑌 )
14		cayleyhamilton0.w	⊢ 𝑊 = ( Base ‘ 𝑌 )
15		cayleyhamilton0.e2	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑌 ) )
16		cayleyhamilton0.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
17		cayleyhamilton0.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 𝑍 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 𝑍 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
18		cayleyhamilton0.u	⊢ 𝑈 = ( 𝑁 cPolyMatToMat 𝑅 )
19		eqid	⊢ ( 𝐶 ‘ 𝑀 ) = ( 𝐶 ‘ 𝑀 )
20	1 2 9 10 11 12 13 16 7 19 17 14 4 5 18 6 15	cayhamlem4	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) ) )
21	8	eqcomi	⊢ ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) = 𝐾
22	21	a1i	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) = 𝐾 )
23	22	fveq1d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) = ( 𝐾 ‘ 𝑛 ) )
24	23	oveq1d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) = ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) )
25	24	mpteq2dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) )
26	25	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) )
27	26	eqeq1d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) ) ↔ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) )
28	27	biimpa	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) ) )
29		oveq1	⊢ ( 𝑛 = 𝑙 → ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) = ( 𝑙 𝐸 ( 𝑇 ‘ 𝑀 ) ) )
30		fveq2	⊢ ( 𝑛 = 𝑙 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑙 ) )
31	29 30	oveq12d	⊢ ( 𝑛 = 𝑙 → ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) = ( ( 𝑙 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑙 ) ) )
32	31	cbvmptv	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) = ( 𝑙 ∈ ℕ0 ↦ ( ( 𝑙 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑙 ) ) )
33	32	oveq2i	⊢ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) = ( 𝑌 Σg ( 𝑙 ∈ ℕ0 ↦ ( ( 𝑙 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑙 ) ) ) )
34	1 2 9 10 11 12 13 16 17 15	cayhamlem1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑙 ∈ ℕ0 ↦ ( ( 𝑙 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑙 ) ) ) ) = 𝑍 )
35	33 34	eqtrid	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) = 𝑍 )
36		fveq2	⊢ ( ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) = 𝑍 → ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) ) = ( 𝑈 ‘ 𝑍 ) )
37		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
38	37	anim2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
39	38	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
40		eqid	⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
41	1 18 9 10 40 13	m2cpminv0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑈 ‘ 𝑍 ) = ( 0g ‘ 𝐴 ) )
42	39 41	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑈 ‘ 𝑍 ) = ( 0g ‘ 𝐴 ) )
43	42 3	eqtr4di	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑈 ‘ 𝑍 ) = 0 )
44	43	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑈 ‘ 𝑍 ) = 0 )
45	36 44	sylan9eqr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) = 𝑍 ) → ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) ) = 0 )
46	35 45	mpdan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) ) = 0 )
47	46	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) → ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) ) = 0 )
48	28 47	eqtrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 )
49	48	ex	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 ) )
50	49	rexlimdvva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 ) )
51	20 50	mpd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 )