Theorem cpmidgsum2

Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as another group sum. (Contributed by AV, 10-Nov-2019)

	Ref	Expression
Hypotheses	cpmadugsum.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	cpmadugsum.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	cpmadugsum.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	cpmadugsum.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
	cpmadugsum.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	cpmadugsum.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	cpmadugsum.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	cpmadugsum.m	⊢ · = ( ·𝑠 ‘ 𝑌 )
	cpmadugsum.r	⊢ × = ( .r ‘ 𝑌 )
	cpmadugsum.1	⊢ 1 = ( 1r ‘ 𝑌 )
	cpmadugsum.g	⊢ + = ( +g ‘ 𝑌 )
	cpmadugsum.s	⊢ − = ( -g ‘ 𝑌 )
	cpmadugsum.i	⊢ 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) )
	cpmadugsum.j	⊢ 𝐽 = ( 𝑁 maAdju 𝑃 )
	cpmadugsum.0	⊢ 0 = ( 0g ‘ 𝑌 )
	cpmadugsum.g2	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
	cpmidgsum2.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	cpmidgsum2.k	⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
	cpmidgsum2.h	⊢ 𝐻 = ( 𝐾 · 1 )
Assertion	cpmidgsum2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) 𝐻 = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cpmadugsum.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		cpmadugsum.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		cpmadugsum.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		cpmadugsum.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5		cpmadugsum.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
6		cpmadugsum.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
7		cpmadugsum.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
8		cpmadugsum.m	⊢ · = ( ·𝑠 ‘ 𝑌 )
9		cpmadugsum.r	⊢ × = ( .r ‘ 𝑌 )
10		cpmadugsum.1	⊢ 1 = ( 1r ‘ 𝑌 )
11		cpmadugsum.g	⊢ + = ( +g ‘ 𝑌 )
12		cpmadugsum.s	⊢ − = ( -g ‘ 𝑌 )
13		cpmadugsum.i	⊢ 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) )
14		cpmadugsum.j	⊢ 𝐽 = ( 𝑁 maAdju 𝑃 )
15		cpmadugsum.0	⊢ 0 = ( 0g ‘ 𝑌 )
16		cpmadugsum.g2	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
17		cpmidgsum2.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
18		cpmidgsum2.k	⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
19		cpmidgsum2.h	⊢ 𝐻 = ( 𝐾 · 1 )
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	cpmadugsum	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) )
21		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
22	21	anim2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
23	22	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
24	3 4	pmatring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
25		ringgrp	⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Grp )
26	23 24 25	3syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Grp )
27	3 4	pmatlmod	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ LMod )
28	21 27	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ LMod )
29	21	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
30		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
31	6 3 30	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
32	29 31	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
33	3	ply1crng	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
34	4	matsca2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
35	33 34	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
36	35	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Base ‘ 𝑃 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
37	32 36	eleqtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
38		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
39	38 10	ringidcl	⊢ ( 𝑌 ∈ Ring → 1 ∈ ( Base ‘ 𝑌 ) )
40	22 24 39	3syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 1 ∈ ( Base ‘ 𝑌 ) )
41		eqid	⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
42		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
43	38 41 8 42	lmodvscl	⊢ ( ( 𝑌 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 1 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
44	28 37 40 43	syl3anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
45	44	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
46	5 1 2 3 4	mat2pmatbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
47	21 46	syl3an2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
48	38 12	grpsubcl	⊢ ( ( 𝑌 ∈ Grp ∧ ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) )
49	26 45 47 48	syl3anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) )
50	33	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ CRing )
51		eqid	⊢ ( 𝑁 maDet 𝑃 ) = ( 𝑁 maDet 𝑃 )
52	4 38 14 51 10 9 8	madurid	⊢ ( ( ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) ∧ 𝑃 ∈ CRing ) → ( ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) × ( 𝐽 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) ) = ( ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) · 1 ) )
53	49 50 52	syl2anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) × ( 𝐽 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) ) = ( ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) · 1 ) )
54		id	⊢ ( 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) → 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) )
55		fveq2	⊢ ( 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) → ( 𝐽 ‘ 𝐼 ) = ( 𝐽 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) )
56	54 55	oveq12d	⊢ ( 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) → ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) × ( 𝐽 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) ) )
57	13 56	mp1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) × ( 𝐽 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) ) )
58	17 1 2 3 4 51 12 6 8 5 10	chpmatval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) = ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) )
59	18 58	eqtrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐾 = ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) )
60	59	oveq1d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐾 · 1 ) = ( ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) · 1 ) )
61	19 60	eqtrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐻 = ( ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) · 1 ) )
62	53 57 61	3eqtr4rd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐻 = ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) )
63	62	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) → 𝐻 = ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) )
64		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) → ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) )
65	63 64	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) → 𝐻 = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) )
66	65	ex	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) → 𝐻 = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) )
67	66	reximdv	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) → ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) 𝐻 = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) )
68	67	reximdv	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) 𝐻 = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) )
69	20 68	mpd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) 𝐻 = ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) )