Theorem cayleyhamilton1

Description: The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation", or, in other words, a matrix over a commutative ring "inserted" into its characteristic polynomial results in zero. In this variant of cayleyhamilton , the meaning of "inserted" is made more transparent: If the characteristic polynomial is a polynomial with coefficients ( Fn ) , then a matrix over a commutative ring "inserted" into its characteristic polynomial is the sum of these coefficients multiplied with the corresponding power of the matrix. (Contributed by AV, 25-Nov-2019)

	Ref	Expression
Hypotheses	cayleyhamilton.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	cayleyhamilton.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	cayleyhamilton.0	⊢ 0 = ( 0g ‘ 𝐴 )
	cayleyhamilton.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	cayleyhamilton.k	⊢ 𝐾 = ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) )
	cayleyhamilton.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
	cayleyhamilton.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐴 ) )
	cayleyhamilton1.l	⊢ 𝐿 = ( Base ‘ 𝑅 )
	cayleyhamilton1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	cayleyhamilton1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	cayleyhamilton1.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
	cayleyhamilton1.e	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	cayleyhamilton1.z	⊢ 𝑍 = ( 0g ‘ 𝑅 )
Assertion	cayleyhamilton1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		cayleyhamilton.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		cayleyhamilton.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		cayleyhamilton.0	⊢ 0 = ( 0g ‘ 𝐴 )
4		cayleyhamilton.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
5		cayleyhamilton.k	⊢ 𝐾 = ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) )
6		cayleyhamilton.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
7		cayleyhamilton.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐴 ) )
8		cayleyhamilton1.l	⊢ 𝐿 = ( Base ‘ 𝑅 )
9		cayleyhamilton1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
10		cayleyhamilton1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
11		cayleyhamilton1.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
12		cayleyhamilton1.e	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
13		cayleyhamilton1.z	⊢ 𝑍 = ( 0g ‘ 𝑅 )
14	1 2 3 4 5 6 7	cayleyhamilton	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 )
15	14	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 )
16		nfv	⊢ Ⅎ 𝑛 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) )
17		nfcv	⊢ Ⅎ 𝑛 𝑃
18		nfcv	⊢ Ⅎ 𝑛 Σg
19		nfmpt1	⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) )
20	17 18 19	nfov	⊢ Ⅎ 𝑛 ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) )
21	20	nfeq2	⊢ Ⅎ 𝑛 ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) )
22	16 21	nfan	⊢ Ⅎ 𝑛 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ∧ ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) )
23		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
24	23	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
25	24	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → 𝑅 ∈ Ring )
26		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
27	4 1 2 10 26	chpmatply1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) ∈ ( Base ‘ 𝑃 ) )
28	27	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( 𝐶 ‘ 𝑀 ) ∈ ( Base ‘ 𝑃 ) )
29		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
30		elmapi	⊢ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) → 𝐹 : ℕ0 ⟶ 𝐿 )
31		ffvelcdm	⊢ ( ( 𝐹 : ℕ0 ⟶ 𝐿 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝐿 )
32	31	ralrimiva	⊢ ( 𝐹 : ℕ0 ⟶ 𝐿 → ∀ 𝑛 ∈ ℕ0 ( 𝐹 ‘ 𝑛 ) ∈ 𝐿 )
33	30 32	syl	⊢ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) → ∀ 𝑛 ∈ ℕ0 ( 𝐹 ‘ 𝑛 ) ∈ 𝐿 )
34	33	ad2antrl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ∀ 𝑛 ∈ ℕ0 ( 𝐹 ‘ 𝑛 ) ∈ 𝐿 )
35	30	feqmptd	⊢ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) → 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐹 ‘ 𝑛 ) ) )
36	13	a1i	⊢ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) → 𝑍 = ( 0g ‘ 𝑅 ) )
37	35 36	breq12d	⊢ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝑛 ∈ ℕ0 ↦ ( 𝐹 ‘ 𝑛 ) ) finSupp ( 0g ‘ 𝑅 ) ) )
38	37	biimpa	⊢ ( ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝐹 ‘ 𝑛 ) ) finSupp ( 0g ‘ 𝑅 ) )
39	38	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝐹 ‘ 𝑛 ) ) finSupp ( 0g ‘ 𝑅 ) )
40	10 26 9 12 25 8 11 29 34 39	gsumsmonply1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) ∈ ( Base ‘ 𝑃 ) )
41		fveq2	⊢ ( 𝑖 = 𝑛 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑛 ) )
42		oveq1	⊢ ( 𝑖 = 𝑛 → ( 𝑖 𝐸 𝑋 ) = ( 𝑛 𝐸 𝑋 ) )
43	41 42	oveq12d	⊢ ( 𝑖 = 𝑛 → ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) = ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) )
44	43	cbvmptv	⊢ ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) )
45	44	oveq2i	⊢ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) )
46	45	fveq2i	⊢ ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) )
47	10 26 5 46	ply1coe1eq	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ‘ 𝑀 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) ∈ ( Base ‘ 𝑃 ) ) → ( ∀ 𝑚 ∈ ℕ0 ( 𝐾 ‘ 𝑚 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑚 ) ↔ ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) ) )
48	25 28 40 47	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( ∀ 𝑚 ∈ ℕ0 ( 𝐾 ‘ 𝑚 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑚 ) ↔ ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) ) )
49		fveq2	⊢ ( 𝑚 = 𝑛 → ( 𝐾 ‘ 𝑚 ) = ( 𝐾 ‘ 𝑛 ) )
50		fveq2	⊢ ( 𝑚 = 𝑛 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑚 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑛 ) )
51	49 50	eqeq12d	⊢ ( 𝑚 = 𝑛 → ( ( 𝐾 ‘ 𝑚 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑚 ) ↔ ( 𝐾 ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑛 ) ) )
52	51	rspcva	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝐾 ‘ 𝑚 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑚 ) ) → ( 𝐾 ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑛 ) )
53		simpl	⊢ ( ( ( 𝐾 ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ) ) → ( 𝐾 ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑛 ) )
54	24	ad2antrl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ) → 𝑅 ∈ Ring )
55		ffvelcdm	⊢ ( ( 𝐹 : ℕ0 ⟶ 𝐿 ∧ 𝑖 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑖 ) ∈ 𝐿 )
56	55	ralrimiva	⊢ ( 𝐹 : ℕ0 ⟶ 𝐿 → ∀ 𝑖 ∈ ℕ0 ( 𝐹 ‘ 𝑖 ) ∈ 𝐿 )
57	30 56	syl	⊢ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) → ∀ 𝑖 ∈ ℕ0 ( 𝐹 ‘ 𝑖 ) ∈ 𝐿 )
58	57	ad2antrl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ∀ 𝑖 ∈ ℕ0 ( 𝐹 ‘ 𝑖 ) ∈ 𝐿 )
59	58	adantl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ) → ∀ 𝑖 ∈ ℕ0 ( 𝐹 ‘ 𝑖 ) ∈ 𝐿 )
60	30	feqmptd	⊢ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) → 𝐹 = ( 𝑖 ∈ ℕ0 ↦ ( 𝐹 ‘ 𝑖 ) ) )
61	60	breq1d	⊢ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝑖 ∈ ℕ0 ↦ ( 𝐹 ‘ 𝑖 ) ) finSupp 𝑍 ) )
62	61	biimpa	⊢ ( ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) → ( 𝑖 ∈ ℕ0 ↦ ( 𝐹 ‘ 𝑖 ) ) finSupp 𝑍 )
63	62	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( 𝑖 ∈ ℕ0 ↦ ( 𝐹 ‘ 𝑖 ) ) finSupp 𝑍 )
64	63	adantl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ) → ( 𝑖 ∈ ℕ0 ↦ ( 𝐹 ‘ 𝑖 ) ) finSupp 𝑍 )
65		simpl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ) → 𝑛 ∈ ℕ0 )
66	10 26 9 12 54 8 11 13 59 64 65	gsummoncoe1	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑛 ) = ⦋ 𝑛 / 𝑖 ⦌ ( 𝐹 ‘ 𝑖 ) )
67		csbfv	⊢ ⦋ 𝑛 / 𝑖 ⦌ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑛 )
68	66 67	eqtrdi	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
69	68	adantl	⊢ ( ( ( 𝐾 ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
70	53 69	eqtrd	⊢ ( ( ( 𝐾 ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ) ) → ( 𝐾 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
71	70	exp32	⊢ ( ( 𝐾 ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑛 ) → ( 𝑛 ∈ ℕ0 → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( 𝐾 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) ) ) )
72	71	com12	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝐾 ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑛 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( 𝐾 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) ) ) )
73	72	adantr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝐾 ‘ 𝑚 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑚 ) ) → ( ( 𝐾 ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑛 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( 𝐾 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) ) ) )
74	52 73	mpd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝐾 ‘ 𝑚 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑚 ) ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( 𝐾 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) ) )
75	74	com12	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝐾 ‘ 𝑚 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑚 ) ) → ( 𝐾 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) ) )
76	75	expcomd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( ∀ 𝑚 ∈ ℕ0 ( 𝐾 ‘ 𝑚 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑖 ) · ( 𝑖 𝐸 𝑋 ) ) ) ) ) ‘ 𝑚 ) → ( 𝑛 ∈ ℕ0 → ( 𝐾 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) ) ) )
77	48 76	sylbird	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) → ( 𝑛 ∈ ℕ0 → ( 𝐾 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) ) ) )
78	77	imp31	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ∧ ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐾 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
79	78	oveq1d	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ∧ ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) = ( ( 𝐹 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) )
80	22 79	mpteq2da	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ∧ ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) )
81	80	oveq2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ∧ ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) )
82	81	eqeq1d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ∧ ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) ) → ( ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 ↔ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 ) )
83	82	biimpd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) ∧ ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) ) → ( ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 ) )
84	83	ex	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) → ( ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 ) ) )
85	15 84	mpid	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝐿 ↑m ℕ0 ) ∧ 𝐹 finSupp 𝑍 ) ) → ( ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) · ( 𝑛 𝐸 𝑋 ) ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 ) )