Theorem chp0mat

Description: The characteristic polynomial of the zero matrix. (Contributed by AV, 18-Aug-2019)

	Ref	Expression
Hypotheses	chp0mat.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	chp0mat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	chp0mat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	chp0mat.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	chp0mat.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
	chp0mat.m	⊢ ↑ = ( .g ‘ 𝐺 )
	chp0mat.0	⊢ 0 = ( 0g ‘ 𝐴 )
Assertion	chp0mat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝐶 ‘ 0 ) = ( ( ♯ ‘ 𝑁 ) ↑ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		chp0mat.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2		chp0mat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		chp0mat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		chp0mat.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
5		chp0mat.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
6		chp0mat.m	⊢ ↑ = ( .g ‘ 𝐺 )
7		chp0mat.0	⊢ 0 = ( 0g ‘ 𝐴 )
8		simpl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑁 ∈ Fin )
9		simpr	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ CRing )
10		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
11	3	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
12	10 11	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ Ring )
13		ringgrp	⊢ ( 𝐴 ∈ Ring → 𝐴 ∈ Grp )
14		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
15	14 7	grpidcl	⊢ ( 𝐴 ∈ Grp → 0 ∈ ( Base ‘ 𝐴 ) )
16	12 13 15	3syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 0 ∈ ( Base ‘ 𝐴 ) )
17		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
18	3 17	mat0op	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐴 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
19	7 18	syl5eq	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 0 = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
20	10 19	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 0 = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
21	20	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 0 = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
22		eqidd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
23		simpl	⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
24	23	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
25		simpr	⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
26	25	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
27		fvexd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 0g ‘ 𝑅 ) ∈ V )
28	21 22 24 26 27	ovmpod	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 0 𝑗 ) = ( 0g ‘ 𝑅 ) )
29	28	a1d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ≠ 𝑗 → ( 𝑖 0 𝑗 ) = ( 0g ‘ 𝑅 ) ) )
30	29	ralrimivva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 0 𝑗 ) = ( 0g ‘ 𝑅 ) ) )
31		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
32		eqid	⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
33	1 2 3 31 14 4 17 5 32	chpdmat	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 0 ∈ ( Base ‘ 𝐴 ) ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 0 𝑗 ) = ( 0g ‘ 𝑅 ) ) ) → ( 𝐶 ‘ 0 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 ( -g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 0 𝑘 ) ) ) ) ) )
34	8 9 16 30 33	syl31anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝐶 ‘ 0 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 ( -g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 0 𝑘 ) ) ) ) ) )
35	20	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → 0 = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
36		eqidd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) ∧ ( 𝑥 = 𝑘 ∧ 𝑦 = 𝑘 ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
37		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
38		fvexd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → ( 0g ‘ 𝑅 ) ∈ V )
39	35 36 37 37 38	ovmpod	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 0 𝑘 ) = ( 0g ‘ 𝑅 ) )
40	39	fveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 0 𝑘 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑅 ) ) )
41	10	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
42		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
43	2 31 17 42	ply1scl0	⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑃 ) )
44	41 43	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑃 ) )
45	44	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑃 ) )
46	40 45	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 0 𝑘 ) ) = ( 0g ‘ 𝑃 ) )
47	46	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑋 ( -g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 0 𝑘 ) ) ) = ( 𝑋 ( -g ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) )
48	2	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
49		ringgrp	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Grp )
50	10 48 49	3syl	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Grp )
51	50	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ Grp )
52		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
53	4 2 52	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
54	41 53	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
55	51 54	jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑃 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) )
56	55	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑃 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) )
57	52 42 32	grpsubid1	⊢ ( ( 𝑃 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑋 ( -g ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) = 𝑋 )
58	56 57	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑋 ( -g ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) = 𝑋 )
59	47 58	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑋 ( -g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 0 𝑘 ) ) ) = 𝑋 )
60	59	mpteq2dva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 ( -g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 0 𝑘 ) ) ) ) = ( 𝑘 ∈ 𝑁 ↦ 𝑋 ) )
61	60	oveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑋 ( -g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 0 𝑘 ) ) ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ 𝑋 ) ) )
62	2	ply1crng	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
63	5	crngmgp	⊢ ( 𝑃 ∈ CRing → 𝐺 ∈ CMnd )
64		cmnmnd	⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
65	62 63 64	3syl	⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ Mnd )
66	65	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐺 ∈ Mnd )
67	10 53	syl	⊢ ( 𝑅 ∈ CRing → 𝑋 ∈ ( Base ‘ 𝑃 ) )
68	67	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
69	5 52	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝐺 )
70	68 69	eleqtrdi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
71		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
72	71 6	gsumconst	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ Fin ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝑁 ) ↑ 𝑋 ) )
73	66 8 70 72	syl3anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝑁 ) ↑ 𝑋 ) )
74	34 61 73	3eqtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝐶 ‘ 0 ) = ( ( ♯ ‘ 𝑁 ) ↑ 𝑋 ) )