chp0mat

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

	Ref	Expression
Hypotheses	chp0mat.c	$⊢ C = N CharPlyMat R$
	chp0mat.p	$⊢ P = {Poly}_{1} (R)$
	chp0mat.a	$⊢ A = N Mat R$
	chp0mat.x	$⊢ X = {var}_{1} (R)$
	chp0mat.g	$⊢ G = {mulGrp}_{P}$
	chp0mat.m	$⊢ \underset{˙}{\times} = \cdot_{G}$
	chp0mat.0	$⊢ \underset{˙}{0} = 0_{A}$
Assertion	chp0mat	$⊢ (N \in Fin \land R \in CRing) \to C (\underset{˙}{0}) = \|N\| \underset{˙}{\times} X$

Proof

Step	Hyp	Ref	Expression
1		chp0mat.c	$⊢ C = N CharPlyMat R$
2		chp0mat.p	$⊢ P = {Poly}_{1} (R)$
3		chp0mat.a	$⊢ A = N Mat R$
4		chp0mat.x	$⊢ X = {var}_{1} (R)$
5		chp0mat.g	$⊢ G = {mulGrp}_{P}$
6		chp0mat.m	$⊢ \underset{˙}{\times} = \cdot_{G}$
7		chp0mat.0	$⊢ \underset{˙}{0} = 0_{A}$
8		simpl	$⊢ (N \in Fin \land R \in CRing) \to N \in Fin$
9		simpr	$⊢ (N \in Fin \land R \in CRing) \to R \in CRing$
10		crngring	$⊢ R \in CRing \to R \in Ring$
11	3	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
12	10 11	sylan2	$⊢ (N \in Fin \land R \in CRing) \to A \in Ring$
13		ringgrp	$⊢ A \in Ring \to A \in Grp$
14		eqid	$⊢ {Base}_{A} = {Base}_{A}$
15	14 7	grpidcl	$⊢ A \in Grp \to \underset{˙}{0} \in {Base}_{A}$
16	12 13 15	3syl	$⊢ (N \in Fin \land R \in CRing) \to \underset{˙}{0} \in {Base}_{A}$
17		eqid	$⊢ 0_{R} = 0_{R}$
18	3 17	mat0op	$⊢ (N \in Fin \land R \in Ring) \to 0_{A} = (x \in N, y \in N ⟼ 0_{R})$
19	7 18	syl5eq	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{0} = (x \in N, y \in N ⟼ 0_{R})$
20	10 19	sylan2	$⊢ (N \in Fin \land R \in CRing) \to \underset{˙}{0} = (x \in N, y \in N ⟼ 0_{R})$
21	20	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (i \in N \land j \in N)) \to \underset{˙}{0} = (x \in N, y \in N ⟼ 0_{R})$
22		eqidd	$⊢ (((N \in Fin \land R \in CRing) \land (i \in N \land j \in N)) \land (x = i \land y = j)) \to 0_{R} = 0_{R}$
23		simpl	$⊢ (i \in N \land j \in N) \to i \in N$
24	23	adantl	$⊢ ((N \in Fin \land R \in CRing) \land (i \in N \land j \in N)) \to i \in N$
25		simpr	$⊢ (i \in N \land j \in N) \to j \in N$
26	25	adantl	$⊢ ((N \in Fin \land R \in CRing) \land (i \in N \land j \in N)) \to j \in N$
27		fvexd	$⊢ ((N \in Fin \land R \in CRing) \land (i \in N \land j \in N)) \to 0_{R} \in V$
28	21 22 24 26 27	ovmpod	$⊢ ((N \in Fin \land R \in CRing) \land (i \in N \land j \in N)) \to i \underset{˙}{0} j = 0_{R}$
29	28	a1d	$⊢ ((N \in Fin \land R \in CRing) \land (i \in N \land j \in N)) \to (i \neq j \to i \underset{˙}{0} j = 0_{R})$
30	29	ralrimivva	$⊢ (N \in Fin \land R \in CRing) \to \forall i \in N \forall j \in N (i \neq j \to i \underset{˙}{0} j = 0_{R})$
31		eqid	$⊢ algSc (P) = algSc (P)$
32		eqid	$⊢ -_{P} = -_{P}$
33	1 2 3 31 14 4 17 5 32	chpdmat	$⊢ ((N \in Fin \land R \in CRing \land \underset{˙}{0} \in {Base}_{A}) \land \forall i \in N \forall j \in N (i \neq j \to i \underset{˙}{0} j = 0_{R})) \to C (\underset{˙}{0}) = \underset{k \in N}{\sum_{G}} (X -_{P} algSc (P) (k \underset{˙}{0} k))$
34	8 9 16 30 33	syl31anc	$⊢ (N \in Fin \land R \in CRing) \to C (\underset{˙}{0}) = \underset{k \in N}{\sum_{G}} (X -_{P} algSc (P) (k \underset{˙}{0} k))$
35	20	adantr	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to \underset{˙}{0} = (x \in N, y \in N ⟼ 0_{R})$
36		eqidd	$⊢ (((N \in Fin \land R \in CRing) \land k \in N) \land (x = k \land y = k)) \to 0_{R} = 0_{R}$
37		simpr	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to k \in N$
38		fvexd	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to 0_{R} \in V$
39	35 36 37 37 38	ovmpod	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to k \underset{˙}{0} k = 0_{R}$
40	39	fveq2d	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to algSc (P) (k \underset{˙}{0} k) = algSc (P) (0_{R})$
41	10	adantl	$⊢ (N \in Fin \land R \in CRing) \to R \in Ring$
42		eqid	$⊢ 0_{P} = 0_{P}$
43	2 31 17 42	ply1scl0	$⊢ R \in Ring \to algSc (P) (0_{R}) = 0_{P}$
44	41 43	syl	$⊢ (N \in Fin \land R \in CRing) \to algSc (P) (0_{R}) = 0_{P}$
45	44	adantr	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to algSc (P) (0_{R}) = 0_{P}$
46	40 45	eqtrd	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to algSc (P) (k \underset{˙}{0} k) = 0_{P}$
47	46	oveq2d	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to X -_{P} algSc (P) (k \underset{˙}{0} k) = X -_{P} 0_{P}$
48	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
49		ringgrp	$⊢ P \in Ring \to P \in Grp$
50	10 48 49	3syl	$⊢ R \in CRing \to P \in Grp$
51	50	adantl	$⊢ (N \in Fin \land R \in CRing) \to P \in Grp$
52		eqid	$⊢ {Base}_{P} = {Base}_{P}$
53	4 2 52	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
54	41 53	syl	$⊢ (N \in Fin \land R \in CRing) \to X \in {Base}_{P}$
55	51 54	jca	$⊢ (N \in Fin \land R \in CRing) \to (P \in Grp \land X \in {Base}_{P})$
56	55	adantr	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to (P \in Grp \land X \in {Base}_{P})$
57	52 42 32	grpsubid1	$⊢ (P \in Grp \land X \in {Base}_{P}) \to X -_{P} 0_{P} = X$
58	56 57	syl	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to X -_{P} 0_{P} = X$
59	47 58	eqtrd	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to X -_{P} algSc (P) (k \underset{˙}{0} k) = X$
60	59	mpteq2dva	$⊢ (N \in Fin \land R \in CRing) \to (k \in N ⟼ X -_{P} algSc (P) (k \underset{˙}{0} k)) = (k \in N ⟼ X)$
61	60	oveq2d	$⊢ (N \in Fin \land R \in CRing) \to \underset{k \in N}{\sum_{G}} (X -_{P} algSc (P) (k \underset{˙}{0} k)) = \underset{k \in N}{\sum_{G}} X$
62	2	ply1crng	$⊢ R \in CRing \to P \in CRing$
63	5	crngmgp	$⊢ P \in CRing \to G \in CMnd$
64		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
65	62 63 64	3syl	$⊢ R \in CRing \to G \in Mnd$
66	65	adantl	$⊢ (N \in Fin \land R \in CRing) \to G \in Mnd$
67	10 53	syl	$⊢ R \in CRing \to X \in {Base}_{P}$
68	67	adantl	$⊢ (N \in Fin \land R \in CRing) \to X \in {Base}_{P}$
69	5 52	mgpbas	$⊢ {Base}_{P} = {Base}_{G}$
70	68 69	eleqtrdi	$⊢ (N \in Fin \land R \in CRing) \to X \in {Base}_{G}$
71		eqid	$⊢ {Base}_{G} = {Base}_{G}$
72	71 6	gsumconst	$⊢ (G \in Mnd \land N \in Fin \land X \in {Base}_{G}) \to \underset{k \in N}{\sum_{G}} X = \|N\| \underset{˙}{\times} X$
73	66 8 70 72	syl3anc	$⊢ (N \in Fin \land R \in CRing) \to \underset{k \in N}{\sum_{G}} X = \|N\| \underset{˙}{\times} X$
74	34 61 73	3eqtrd	$⊢ (N \in Fin \land R \in CRing) \to C (\underset{˙}{0}) = \|N\| \underset{˙}{\times} X$

Metamath Proof Explorer

Theorem chp0mat

Proof