chpscmatgsumbin

Description: The characteristic polynomial of a (nonempty!) scalar matrix, expressed as finite group sum of binomials. (Contributed by AV, 2-Sep-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}$
	chpscmat.d	$⊢ D = \{m \in {Base}_{A} \| \exists c \in {Base}_{R} \forall i \in N \forall j \in N i m j = if (i = j, c, 0_{R})\}$
	chpscmat.s	$⊢ S = algSc (P)$
	chpscmat.m	$⊢ \underset{˙}{-} = -_{P}$
	chpscmatgsum.f	$⊢ F = \cdot_{P}$
	chpscmatgsum.h	$⊢ H = {mulGrp}_{R}$
	chpscmatgsum.e	$⊢ E = \cdot_{H}$
	chpscmatgsum.i	$⊢ I = {inv}_{g} (R)$
	chpscmatgsum.s	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
Assertion	chpscmatgsumbin	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to C (M) = {\sum_{P}}_{l = 0}^{\|N\|} ((\binom{\|N\|}{l}) F (((\|N\| - l) E I (J M J)) \underset{˙}{\cdot} (l \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		chpscmat.d	$⊢ D = \{m \in {Base}_{A} \| \exists c \in {Base}_{R} \forall i \in N \forall j \in N i m j = if (i = j, c, 0_{R})\}$
8		chpscmat.s	$⊢ S = algSc (P)$
9		chpscmat.m	$⊢ \underset{˙}{-} = -_{P}$
10		chpscmatgsum.f	$⊢ F = \cdot_{P}$
11		chpscmatgsum.h	$⊢ H = {mulGrp}_{R}$
12		chpscmatgsum.e	$⊢ E = \cdot_{H}$
13		chpscmatgsum.i	$⊢ I = {inv}_{g} (R)$
14		chpscmatgsum.s	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
15	1 2 3 4 5 6 7 8 9	chpscmat0	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to C (M) = \|N\| \underset{˙}{\times} (X \underset{˙}{-} S (J M J))$
16		crngring	$⊢ R \in CRing \to R \in Ring$
17	16	adantl	$⊢ (N \in Fin \land R \in CRing) \to R \in Ring$
18		eqid	$⊢ {Base}_{P} = {Base}_{P}$
19	4 2 18	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
20	17 19	syl	$⊢ (N \in Fin \land R \in CRing) \to X \in {Base}_{P}$
21	20	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to X \in {Base}_{P}$
22	16	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to R \in Ring$
23		eqid	$⊢ Scalar (P) = Scalar (P)$
24	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
25	2	ply1lmod	$⊢ R \in Ring \to P \in LMod$
26		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
27	8 23 24 25 26 18	asclf	$⊢ R \in Ring \to S : {Base}_{Scalar (P)} ⟶ {Base}_{P}$
28	22 27	syl	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to S : {Base}_{Scalar (P)} ⟶ {Base}_{P}$
29		simpr2	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to J \in N$
30		elrabi	$⊢ M \in \{m \in {Base}_{A} \| \exists c \in {Base}_{R} \forall i \in N \forall j \in N i m j = if (i = j, c, 0_{R})\} \to M \in {Base}_{A}$
31	30	a1d	$⊢ M \in \{m \in {Base}_{A} \| \exists c \in {Base}_{R} \forall i \in N \forall j \in N i m j = if (i = j, c, 0_{R})\} \to ((N \in Fin \land R \in CRing) \to M \in {Base}_{A})$
32	31 7	eleq2s	$⊢ M \in D \to ((N \in Fin \land R \in CRing) \to M \in {Base}_{A})$
33	32	3ad2ant1	$⊢ (M \in D \land J \in N \land \forall n \in N n M n = J M J) \to ((N \in Fin \land R \in CRing) \to M \in {Base}_{A})$
34	33	impcom	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to M \in {Base}_{A}$
35		eqid	$⊢ {Base}_{R} = {Base}_{R}$
36	3 35	matecl	$⊢ (J \in N \land J \in N \land M \in {Base}_{A}) \to J M J \in {Base}_{R}$
37	29 29 34 36	syl3anc	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to J M J \in {Base}_{R}$
38	2	ply1sca	$⊢ R \in CRing \to R = Scalar (P)$
39	38	adantl	$⊢ (N \in Fin \land R \in CRing) \to R = Scalar (P)$
40	39	eqcomd	$⊢ (N \in Fin \land R \in CRing) \to Scalar (P) = R$
41	40	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to Scalar (P) = R$
42	41	fveq2d	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to {Base}_{Scalar (P)} = {Base}_{R}$
43	37 42	eleqtrrd	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to J M J \in {Base}_{Scalar (P)}$
44	28 43	ffvelrnd	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to S (J M J) \in {Base}_{P}$
45		eqid	$⊢ +_{P} = +_{P}$
46		eqid	$⊢ {inv}_{g} (P) = {inv}_{g} (P)$
47	18 45 46 9	grpsubval	$⊢ (X \in {Base}_{P} \land S (J M J) \in {Base}_{P}) \to X \underset{˙}{-} S (J M J) = X +_{P} {inv}_{g} (P) (S (J M J))$
48	21 44 47	syl2anc	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to X \underset{˙}{-} S (J M J) = X +_{P} {inv}_{g} (P) (S (J M J))$
49	17 25	syl	$⊢ (N \in Fin \land R \in CRing) \to P \in LMod$
50	49	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to P \in LMod$
51	17 24	syl	$⊢ (N \in Fin \land R \in CRing) \to P \in Ring$
52	51	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to P \in Ring$
53		eqid	$⊢ {inv}_{g} (Scalar (P)) = {inv}_{g} (Scalar (P))$
54	8 23 26 53 46	asclinvg	$⊢ (P \in LMod \land P \in Ring \land J M J \in {Base}_{Scalar (P)}) \to {inv}_{g} (P) (S (J M J)) = S ({inv}_{g} (Scalar (P)) (J M J))$
55	50 52 43 54	syl3anc	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to {inv}_{g} (P) (S (J M J)) = S ({inv}_{g} (Scalar (P)) (J M J))$
56	39	fveq2d	$⊢ (N \in Fin \land R \in CRing) \to {inv}_{g} (R) = {inv}_{g} (Scalar (P))$
57	56	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to {inv}_{g} (R) = {inv}_{g} (Scalar (P))$
58	13 57	eqtr2id	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to {inv}_{g} (Scalar (P)) = I$
59	58	fveq1d	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to {inv}_{g} (Scalar (P)) (J M J) = I (J M J)$
60	59	fveq2d	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to S ({inv}_{g} (Scalar (P)) (J M J)) = S (I (J M J))$
61	55 60	eqtrd	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to {inv}_{g} (P) (S (J M J)) = S (I (J M J))$
62	61	oveq2d	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to X +_{P} {inv}_{g} (P) (S (J M J)) = X +_{P} S (I (J M J))$
63	48 62	eqtrd	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to X \underset{˙}{-} S (J M J) = X +_{P} S (I (J M J))$
64	63	oveq2d	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to \|N\| \underset{˙}{\times} (X \underset{˙}{-} S (J M J)) = \|N\| \underset{˙}{\times} (X +_{P} S (I (J M J)))$
65		simplr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to R \in CRing$
66		hashcl	$⊢ N \in Fin \to \|N\| \in ℕ_{0}$
67	66	ad2antrr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to \|N\| \in ℕ_{0}$
68		ringgrp	$⊢ R \in Ring \to R \in Grp$
69	16 68	syl	$⊢ R \in CRing \to R \in Grp$
70	69	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to R \in Grp$
71	35 13	grpinvcl	$⊢ (R \in Grp \land J M J \in {Base}_{R}) \to I (J M J) \in {Base}_{R}$
72	70 37 71	syl2anc	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to I (J M J) \in {Base}_{R}$
73		eqid	$⊢ \cdot_{P} = \cdot_{P}$
74	2 4 45 73 10 5 6 35 8 11 12	lply1binomsc	$⊢ (R \in CRing \land \|N\| \in ℕ_{0} \land I (J M J) \in {Base}_{R}) \to \|N\| \underset{˙}{\times} (X +_{P} S (I (J M J))) = {\sum_{P}}_{l = 0}^{\|N\|} ((\binom{\|N\|}{l}) F (S ((\|N\| - l) E I (J M J)) \cdot_{P} (l \underset{˙}{\times} X)))$
75	65 67 72 74	syl3anc	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to \|N\| \underset{˙}{\times} (X +_{P} S (I (J M J))) = {\sum_{P}}_{l = 0}^{\|N\|} ((\binom{\|N\|}{l}) F (S ((\|N\| - l) E I (J M J)) \cdot_{P} (l \underset{˙}{\times} X)))$
76	2	ply1assa	$⊢ R \in CRing \to P \in AssAlg$
77	76	adantl	$⊢ (N \in Fin \land R \in CRing) \to P \in AssAlg$
78	77	ad2antrr	$⊢ (((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \land l \in (0 \dots \|N\|)) \to P \in AssAlg$
79	11	ringmgp	$⊢ R \in Ring \to H \in Mnd$
80	17 79	syl	$⊢ (N \in Fin \land R \in CRing) \to H \in Mnd$
81	80	ad2antrr	$⊢ (((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \land l \in (0 \dots \|N\|)) \to H \in Mnd$
82		fznn0sub	$⊢ l \in (0 \dots \|N\|) \to \|N\| - l \in ℕ_{0}$
83	82	adantl	$⊢ (((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \land l \in (0 \dots \|N\|)) \to \|N\| - l \in ℕ_{0}$
84	11 35	mgpbas	$⊢ {Base}_{R} = {Base}_{H}$
85	72 84	eleqtrdi	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to I (J M J) \in {Base}_{H}$
86	85	adantr	$⊢ (((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \land l \in (0 \dots \|N\|)) \to I (J M J) \in {Base}_{H}$
87		eqid	$⊢ {Base}_{H} = {Base}_{H}$
88	87 12	mulgnn0cl	$⊢ (H \in Mnd \land \|N\| - l \in ℕ_{0} \land I (J M J) \in {Base}_{H}) \to (\|N\| - l) E I (J M J) \in {Base}_{H}$
89	81 83 86 88	syl3anc	$⊢ (((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \land l \in (0 \dots \|N\|)) \to (\|N\| - l) E I (J M J) \in {Base}_{H}$
90	40	fveq2d	$⊢ (N \in Fin \land R \in CRing) \to {Base}_{Scalar (P)} = {Base}_{R}$
91	90 84	eqtrdi	$⊢ (N \in Fin \land R \in CRing) \to {Base}_{Scalar (P)} = {Base}_{H}$
92	91	ad2antrr	$⊢ (((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \land l \in (0 \dots \|N\|)) \to {Base}_{Scalar (P)} = {Base}_{H}$
93	89 92	eleqtrrd	$⊢ (((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \land l \in (0 \dots \|N\|)) \to (\|N\| - l) E I (J M J) \in {Base}_{Scalar (P)}$
94	5	ringmgp	$⊢ P \in Ring \to G \in Mnd$
95	16 24 94	3syl	$⊢ R \in CRing \to G \in Mnd$
96	95	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land l \in (0 \dots \|N\|)) \to G \in Mnd$
97		elfznn0	$⊢ l \in (0 \dots \|N\|) \to l \in ℕ_{0}$
98	97	adantl	$⊢ ((N \in Fin \land R \in CRing) \land l \in (0 \dots \|N\|)) \to l \in ℕ_{0}$
99	20	adantr	$⊢ ((N \in Fin \land R \in CRing) \land l \in (0 \dots \|N\|)) \to X \in {Base}_{P}$
100	5 18	mgpbas	$⊢ {Base}_{P} = {Base}_{G}$
101	100 6	mulgnn0cl	$⊢ (G \in Mnd \land l \in ℕ_{0} \land X \in {Base}_{P}) \to l \underset{˙}{\times} X \in {Base}_{P}$
102	96 98 99 101	syl3anc	$⊢ ((N \in Fin \land R \in CRing) \land l \in (0 \dots \|N\|)) \to l \underset{˙}{\times} X \in {Base}_{P}$
103	102	adantlr	$⊢ (((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \land l \in (0 \dots \|N\|)) \to l \underset{˙}{\times} X \in {Base}_{P}$
104	8 23 26 18 73 14	asclmul1	$⊢ (P \in AssAlg \land (\|N\| - l) E I (J M J) \in {Base}_{Scalar (P)} \land l \underset{˙}{\times} X \in {Base}_{P}) \to S ((\|N\| - l) E I (J M J)) \cdot_{P} (l \underset{˙}{\times} X) = ((\|N\| - l) E I (J M J)) \underset{˙}{\cdot} (l \underset{˙}{\times} X)$
105	78 93 103 104	syl3anc	$⊢ (((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \land l \in (0 \dots \|N\|)) \to S ((\|N\| - l) E I (J M J)) \cdot_{P} (l \underset{˙}{\times} X) = ((\|N\| - l) E I (J M J)) \underset{˙}{\cdot} (l \underset{˙}{\times} X)$
106	105	oveq2d	$⊢ (((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \land l \in (0 \dots \|N\|)) \to (\binom{\|N\|}{l}) F (S ((\|N\| - l) E I (J M J)) \cdot_{P} (l \underset{˙}{\times} X)) = (\binom{\|N\|}{l}) F (((\|N\| - l) E I (J M J)) \underset{˙}{\cdot} (l \underset{˙}{\times} X))$
107	106	mpteq2dva	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to (l \in (0 \dots \|N\|) ⟼ (\binom{\|N\|}{l}) F (S ((\|N\| - l) E I (J M J)) \cdot_{P} (l \underset{˙}{\times} X))) = (l \in (0 \dots \|N\|) ⟼ (\binom{\|N\|}{l}) F (((\|N\| - l) E I (J M J)) \underset{˙}{\cdot} (l \underset{˙}{\times} X)))$
108	107	oveq2d	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to {\sum_{P}}_{l = 0}^{\|N\|} ((\binom{\|N\|}{l}) F (S ((\|N\| - l) E I (J M J)) \cdot_{P} (l \underset{˙}{\times} X))) = {\sum_{P}}_{l = 0}^{\|N\|} ((\binom{\|N\|}{l}) F (((\|N\| - l) E I (J M J)) \underset{˙}{\cdot} (l \underset{˙}{\times} X)))$
109	75 108	eqtrd	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to \|N\| \underset{˙}{\times} (X +_{P} S (I (J M J))) = {\sum_{P}}_{l = 0}^{\|N\|} ((\binom{\|N\|}{l}) F (((\|N\| - l) E I (J M J)) \underset{˙}{\cdot} (l \underset{˙}{\times} X)))$
110	15 64 109	3eqtrd	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land J \in N \land \forall n \in N n M n = J M J)) \to C (M) = {\sum_{P}}_{l = 0}^{\|N\|} ((\binom{\|N\|}{l}) F (((\|N\| - l) E I (J M J)) \underset{˙}{\cdot} (l \underset{˙}{\times} X)))$

Metamath Proof Explorer

Theorem chpscmatgsumbin

Proof