chcoeffeq

Description: The coefficients of the characteristic polynomial multiplied with the identity matrix represented by (transformed) ring elements obtained from the adjunct of the characteristic matrix. (Contributed by AV, 21-Nov-2019) (Proof shortened by AV, 8-Dec-2019) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	chcoeffeq.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	chcoeffeq.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	chcoeffeq.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	chcoeffeq.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
	chcoeffeq.r	⊢ × = ( ._r ‘ 𝑌 )
	chcoeffeq.s	⊢ − = ( -_g ‘ 𝑌 )
	chcoeffeq.0	⊢ 0 = ( 0_g ‘ 𝑌 )
	chcoeffeq.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	chcoeffeq.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	chcoeffeq.k	⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
	chcoeffeq.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ₀ ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
	chcoeffeq.w	⊢ 𝑊 = ( Base ‘ 𝑌 )
	chcoeffeq.1	⊢ 1 = ( 1_r ‘ 𝐴 )
	chcoeffeq.m	⊢ ∗ = ( ·_𝑠 ‘ 𝐴 )
	chcoeffeq.u	⊢ 𝑈 = ( 𝑁 cPolyMatToMat 𝑅 )
Assertion	chcoeffeq	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ∀ 𝑛 ∈ ℕ₀ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) )

Proof

Step	Hyp	Ref	Expression
1		chcoeffeq.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		chcoeffeq.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		chcoeffeq.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
4		chcoeffeq.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5		chcoeffeq.r	⊢ × = ( ._r ‘ 𝑌 )
6		chcoeffeq.s	⊢ − = ( -_g ‘ 𝑌 )
7		chcoeffeq.0	⊢ 0 = ( 0_g ‘ 𝑌 )
8		chcoeffeq.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
9		chcoeffeq.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
10		chcoeffeq.k	⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
11		chcoeffeq.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ₀ ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
12		chcoeffeq.w	⊢ 𝑊 = ( Base ‘ 𝑌 )
13		chcoeffeq.1	⊢ 1 = ( 1_r ‘ 𝐴 )
14		chcoeffeq.m	⊢ ∗ = ( ·_𝑠 ‘ 𝐴 )
15		chcoeffeq.u	⊢ 𝑈 = ( 𝑁 cPolyMatToMat 𝑅 )
16		eqid	⊢ ( 𝑁 ConstPolyMat 𝑅 ) = ( 𝑁 ConstPolyMat 𝑅 )
17		eqid	⊢ ( ·_𝑠 ‘ 𝑌 ) = ( ·_𝑠 ‘ 𝑌 )
18		eqid	⊢ ( 1_r ‘ 𝑌 ) = ( 1_r ‘ 𝑌 )
19		eqid	⊢ ( var₁ ‘ 𝑅 ) = ( var₁ ‘ 𝑅 )
20		eqid	⊢ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) = ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) )
21		eqid	⊢ ( 𝑁 maAdju 𝑃 ) = ( 𝑁 maAdju 𝑃 )
22		eqid	⊢ ( Poly₁ ‘ 𝐴 ) = ( Poly₁ ‘ 𝐴 )
23		eqid	⊢ ( var₁ ‘ 𝐴 ) = ( var₁ ‘ 𝐴 )
24		eqid	⊢ ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) = ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) )
25		eqid	⊢ ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) = ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) )
26		eqid	⊢ ( 𝑁 pMatToMatPoly 𝑅 ) = ( 𝑁 pMatToMatPoly 𝑅 )
27	1 2 3 4 8 5 6 7 11 16 17 18 19 20 21 12 22 23 24 25 15 26	cpmadumatpoly	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) )
28		eqid	⊢ ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) = ( ._g ‘ ( mulGrp ‘ 𝑃 ) )
29		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
30		eqid	⊢ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) = ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) )
31	1 2 3 4 19 28 17 18 29 9 10 30 13 14 8 12 22 23 24 25 26	cpmidpmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) )
32		eqid	⊢ ( 𝑁 CharPlyMat 𝑅 ) = ( 𝑁 CharPlyMat 𝑅 )
33	1 2 32 3 4 19 8 6 17 18 20 21 5	cpmadurid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) = ( ( ( 𝑁 CharPlyMat 𝑅 ) ‘ 𝑀 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) )
34	9	fveq1i	⊢ ( 𝐶 ‘ 𝑀 ) = ( ( 𝑁 CharPlyMat 𝑅 ) ‘ 𝑀 )
35	10 34	eqtri	⊢ 𝐾 = ( ( 𝑁 CharPlyMat 𝑅 ) ‘ 𝑀 )
36	35	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐾 = ( ( 𝑁 CharPlyMat 𝑅 ) ‘ 𝑀 ) )
37	36	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 CharPlyMat 𝑅 ) ‘ 𝑀 ) = 𝐾 )
38	37	oveq1d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( ( 𝑁 CharPlyMat 𝑅 ) ‘ 𝑀 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) = ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) )
39	33 38	eqtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) = ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) )
40		fveq2	⊢ ( ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) = ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) → ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) )
41		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ) ) ∧ ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) ) → ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) )
42	41	adantr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ) ) ∧ ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) ) ∧ ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) ) → ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) )
43		simpr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ) ) ∧ ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) ) ∧ ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) ) → ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) )
44	42 43	eqeq12d	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ) ) ∧ ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) ) ∧ ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) ↔ ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) ) )
45	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	chcoeffeqlem	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ) ) → ( ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ₀ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) )
46	45	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ) ) ∧ ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) ) → ( ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ₀ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) )
47	46	adantr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ) ) ∧ ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) ) ∧ ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) ) → ( ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ₀ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) )
48	44 47	sylbid	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ) ) ∧ ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) ) ∧ ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) → ∀ 𝑛 ∈ ℕ₀ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) )
49	48	exp31	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) → ∀ 𝑛 ∈ ℕ₀ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) ) ) )
50	49	com24	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ₀ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) ) ) )
51	40 50	syl5	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) = ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ₀ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) ) ) )
52	51	ex	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ) → ( ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) = ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ₀ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) ) ) ) )
53	52	com24	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ( ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) = ( 𝐾 ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) → ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ₀ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) ) ) ) )
54	31 39 53	mp2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ₀ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) ) )
55	54	impl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ) → ( ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ₀ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) )
56	55	reximdva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) → ( ∃ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ∃ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ∀ 𝑛 ∈ ℕ₀ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) )
57	56	reximdva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ( ( 𝑁 pMatToMatPoly 𝑅 ) ‘ ( ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑁 maAdju 𝑃 ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑌 ) ( 1_r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) ) ) ) = ( ( Poly₁ ‘ 𝐴 ) Σ_g ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·_𝑠 ‘ ( Poly₁ ‘ 𝐴 ) ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐴 ) ) ) ( var₁ ‘ 𝐴 ) ) ) ) ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ∀ 𝑛 ∈ ℕ₀ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) )
58	27 57	mpd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑_m ( 0 ... 𝑠 ) ) ∀ 𝑛 ∈ ℕ₀ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) )

Metamath Proof Explorer

Theorem chcoeffeq

Proof