chpidmat

Description: The characteristic polynomial of the identity matrix. (Contributed by AV, 19-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}$
	chpidmat.i	$⊢ I = 1_{A}$
	chpidmat.s	$⊢ S = algSc (P)$
	chpidmat.1	$⊢ \underset{˙}{1} = 1_{R}$
	chpidmat.m	$⊢ \underset{˙}{-} = -_{P}$
Assertion	chpidmat	$⊢ (N \in Fin \land R \in CRing) \to C (I) = \|N\| \underset{˙}{\times} (X \underset{˙}{-} S (\underset{˙}{1}))$

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		chpidmat.i	$⊢ I = 1_{A}$
8		chpidmat.s	$⊢ S = algSc (P)$
9		chpidmat.1	$⊢ \underset{˙}{1} = 1_{R}$
10		chpidmat.m	$⊢ \underset{˙}{-} = -_{P}$
11		simpl	$⊢ (N \in Fin \land R \in CRing) \to N \in Fin$
12		simpr	$⊢ (N \in Fin \land R \in CRing) \to R \in CRing$
13		crngring	$⊢ R \in CRing \to R \in Ring$
14	3	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
15	13 14	sylan2	$⊢ (N \in Fin \land R \in CRing) \to A \in Ring$
16		eqid	$⊢ {Base}_{A} = {Base}_{A}$
17	16 7	ringidcl	$⊢ A \in Ring \to I \in {Base}_{A}$
18	15 17	syl	$⊢ (N \in Fin \land R \in CRing) \to I \in {Base}_{A}$
19		eqid	$⊢ 0_{R} = 0_{R}$
20	11	ad2antrr	$⊢ (((N \in Fin \land R \in CRing) \land (i \in N \land j \in N)) \land i \neq j) \to N \in Fin$
21	13	adantl	$⊢ (N \in Fin \land R \in CRing) \to R \in Ring$
22	21	ad2antrr	$⊢ (((N \in Fin \land R \in CRing) \land (i \in N \land j \in N)) \land i \neq j) \to R \in Ring$
23		simplrl	$⊢ (((N \in Fin \land R \in CRing) \land (i \in N \land j \in N)) \land i \neq j) \to i \in N$
24		simplrr	$⊢ (((N \in Fin \land R \in CRing) \land (i \in N \land j \in N)) \land i \neq j) \to j \in N$
25	3 9 19 20 22 23 24 7	mat1ov	$⊢ (((N \in Fin \land R \in CRing) \land (i \in N \land j \in N)) \land i \neq j) \to i I j = if (i = j, \underset{˙}{1}, 0_{R})$
26		ifnefalse	$⊢ i \neq j \to if (i = j, \underset{˙}{1}, 0_{R}) = 0_{R}$
27	26	adantl	$⊢ (((N \in Fin \land R \in CRing) \land (i \in N \land j \in N)) \land i \neq j) \to if (i = j, \underset{˙}{1}, 0_{R}) = 0_{R}$
28	25 27	eqtrd	$⊢ (((N \in Fin \land R \in CRing) \land (i \in N \land j \in N)) \land i \neq j) \to i I j = 0_{R}$
29	28	ex	$⊢ ((N \in Fin \land R \in CRing) \land (i \in N \land j \in N)) \to (i \neq j \to i I 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 I j = 0_{R})$
31		eqid	$⊢ -_{P} = -_{P}$
32	1 2 3 8 16 4 19 5 31	chpdmat	$⊢ ((N \in Fin \land R \in CRing \land I \in {Base}_{A}) \land \forall i \in N \forall j \in N (i \neq j \to i I j = 0_{R})) \to C (I) = \underset{k \in N}{\sum_{G}} (X -_{P} S (k I k))$
33	11 12 18 30 32	syl31anc	$⊢ (N \in Fin \land R \in CRing) \to C (I) = \underset{k \in N}{\sum_{G}} (X -_{P} S (k I k))$
34	11	adantr	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to N \in Fin$
35	21	adantr	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to R \in Ring$
36		simpr	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to k \in N$
37	3 9 19 34 35 36 36 7	mat1ov	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to k I k = if (k = k, \underset{˙}{1}, 0_{R})$
38		eqid	$⊢ k = k$
39	38	iftruei	$⊢ if (k = k, \underset{˙}{1}, 0_{R}) = \underset{˙}{1}$
40	37 39	eqtrdi	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to k I k = \underset{˙}{1}$
41	40	fveq2d	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to S (k I k) = S (\underset{˙}{1})$
42	41	oveq2d	$⊢ ((N \in Fin \land R \in CRing) \land k \in N) \to X -_{P} S (k I k) = X -_{P} S (\underset{˙}{1})$
43	42	mpteq2dva	$⊢ (N \in Fin \land R \in CRing) \to (k \in N ⟼ X -_{P} S (k I k)) = (k \in N ⟼ X -_{P} S (\underset{˙}{1}))$
44	43	oveq2d	$⊢ (N \in Fin \land R \in CRing) \to \underset{k \in N}{\sum_{G}} (X -_{P} S (k I k)) = \underset{k \in N}{\sum_{G}} (X -_{P} S (\underset{˙}{1}))$
45	2	ply1crng	$⊢ R \in CRing \to P \in CRing$
46	5	crngmgp	$⊢ P \in CRing \to G \in CMnd$
47		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
48	45 46 47	3syl	$⊢ R \in CRing \to G \in Mnd$
49	48	adantl	$⊢ (N \in Fin \land R \in CRing) \to G \in Mnd$
50	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
51		ringgrp	$⊢ P \in Ring \to P \in Grp$
52	50 51	syl	$⊢ R \in Ring \to P \in Grp$
53		eqid	$⊢ {Base}_{P} = {Base}_{P}$
54	4 2 53	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
55		eqid	$⊢ 1_{P} = 1_{P}$
56	2 8 9 55	ply1scl1	$⊢ R \in Ring \to S (\underset{˙}{1}) = 1_{P}$
57	53 55	ringidcl	$⊢ P \in Ring \to 1_{P} \in {Base}_{P}$
58	50 57	syl	$⊢ R \in Ring \to 1_{P} \in {Base}_{P}$
59	56 58	eqeltrd	$⊢ R \in Ring \to S (\underset{˙}{1}) \in {Base}_{P}$
60	52 54 59	3jca	$⊢ R \in Ring \to (P \in Grp \land X \in {Base}_{P} \land S (\underset{˙}{1}) \in {Base}_{P})$
61	13 60	syl	$⊢ R \in CRing \to (P \in Grp \land X \in {Base}_{P} \land S (\underset{˙}{1}) \in {Base}_{P})$
62	61	adantl	$⊢ (N \in Fin \land R \in CRing) \to (P \in Grp \land X \in {Base}_{P} \land S (\underset{˙}{1}) \in {Base}_{P})$
63	53 31	grpsubcl	$⊢ (P \in Grp \land X \in {Base}_{P} \land S (\underset{˙}{1}) \in {Base}_{P}) \to X -_{P} S (\underset{˙}{1}) \in {Base}_{P}$
64	62 63	syl	$⊢ (N \in Fin \land R \in CRing) \to X -_{P} S (\underset{˙}{1}) \in {Base}_{P}$
65	5 53	mgpbas	$⊢ {Base}_{P} = {Base}_{G}$
66	64 65	eleqtrdi	$⊢ (N \in Fin \land R \in CRing) \to X -_{P} S (\underset{˙}{1}) \in {Base}_{G}$
67		eqid	$⊢ {Base}_{G} = {Base}_{G}$
68	67 6	gsumconst	$⊢ (G \in Mnd \land N \in Fin \land X -_{P} S (\underset{˙}{1}) \in {Base}_{G}) \to \underset{k \in N}{\sum_{G}} (X -_{P} S (\underset{˙}{1})) = \|N\| \underset{˙}{\times} (X -_{P} S (\underset{˙}{1}))$
69	10	eqcomi	$⊢ -_{P} = \underset{˙}{-}$
70	69	oveqi	$⊢ X -_{P} S (\underset{˙}{1}) = X \underset{˙}{-} S (\underset{˙}{1})$
71	70	oveq2i	$⊢ \|N\| \underset{˙}{\times} (X -_{P} S (\underset{˙}{1})) = \|N\| \underset{˙}{\times} (X \underset{˙}{-} S (\underset{˙}{1}))$
72	68 71	eqtrdi	$⊢ (G \in Mnd \land N \in Fin \land X -_{P} S (\underset{˙}{1}) \in {Base}_{G}) \to \underset{k \in N}{\sum_{G}} (X -_{P} S (\underset{˙}{1})) = \|N\| \underset{˙}{\times} (X \underset{˙}{-} S (\underset{˙}{1}))$
73	49 11 66 72	syl3anc	$⊢ (N \in Fin \land R \in CRing) \to \underset{k \in N}{\sum_{G}} (X -_{P} S (\underset{˙}{1})) = \|N\| \underset{˙}{\times} (X \underset{˙}{-} S (\underset{˙}{1}))$
74	44 73	eqtrd	$⊢ (N \in Fin \land R \in CRing) \to \underset{k \in N}{\sum_{G}} (X -_{P} S (k I k)) = \|N\| \underset{˙}{\times} (X \underset{˙}{-} S (\underset{˙}{1}))$
75	33 74	eqtrd	$⊢ (N \in Fin \land R \in CRing) \to C (I) = \|N\| \underset{˙}{\times} (X \underset{˙}{-} S (\underset{˙}{1}))$

Metamath Proof Explorer

Theorem chpidmat

Proof