chpscmatgsummon

Description: The characteristic polynomial of a (nonempty!) scalar matrix, expressed as finite group sum of scaled monomials. (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}$
	chpscmatgsum.z	$⊢ Z = \cdot_{R}$
Assertion	chpscmatgsummon	$⊢ ((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}) Z ((\|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		chpscmatgsum.z	$⊢ Z = \cdot_{R}$
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14	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)))$
17		crngring	$⊢ R \in CRing \to R \in Ring$
18	17	adantl	$⊢ (N \in Fin \land R \in CRing) \to R \in Ring$
19	2	ply1lmod	$⊢ R \in Ring \to P \in LMod$
20	18 19	syl	$⊢ (N \in Fin \land R \in CRing) \to P \in LMod$
21	20	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 LMod$
22		eqid	$⊢ {Base}_{R} = {Base}_{R}$
23	11 22	mgpbas	$⊢ {Base}_{R} = {Base}_{H}$
24	11	ringmgp	$⊢ R \in Ring \to H \in Mnd$
25	18 24	syl	$⊢ (N \in Fin \land R \in CRing) \to H \in Mnd$
26	25	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$
27		fznn0sub	$⊢ l \in (0 \dots \|N\|) \to \|N\| - l \in ℕ_{0}$
28	27	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}$
29		ringgrp	$⊢ R \in Ring \to R \in Grp$
30	17 29	syl	$⊢ R \in CRing \to R \in Grp$
31	30	adantl	$⊢ (N \in Fin \land R \in CRing) \to R \in Grp$
32		simp2	$⊢ (M \in D \land J \in N \land \forall n \in N n M n = J M J) \to J \in N$
33		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}$
34	33 7	eleq2s	$⊢ M \in D \to M \in {Base}_{A}$
35	34	3ad2ant1	$⊢ (M \in D \land J \in N \land \forall n \in N n M n = J M J) \to M \in {Base}_{A}$
36	32 32 35	3jca	$⊢ (M \in D \land J \in N \land \forall n \in N n M n = J M J) \to (J \in N \land J \in N \land M \in {Base}_{A})$
37	36	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)) \to (J \in N \land J \in N \land M \in {Base}_{A})$
38	3 22	matecl	$⊢ (J \in N \land J \in N \land M \in {Base}_{A}) \to J M J \in {Base}_{R}$
39	37 38	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 J M J \in {Base}_{R}$
40	22 13	grpinvcl	$⊢ (R \in Grp \land J M J \in {Base}_{R}) \to I (J M J) \in {Base}_{R}$
41	31 39 40	syl2an2r	$⊢ ((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}$
42	41	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}_{R}$
43	23 12 26 28 42	mulgnn0cld	$⊢ (((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}_{R}$
44	2	ply1sca	$⊢ R \in CRing \to R = Scalar (P)$
45	44	adantl	$⊢ (N \in Fin \land R \in CRing) \to R = Scalar (P)$
46	45	eqcomd	$⊢ (N \in Fin \land R \in CRing) \to Scalar (P) = R$
47	46	fveq2d	$⊢ (N \in Fin \land R \in CRing) \to {Base}_{Scalar (P)} = {Base}_{R}$
48	47	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}_{R}$
49	43 48	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)}$
50		hashcl	$⊢ N \in Fin \to \|N\| \in ℕ_{0}$
51	50	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}$
52		elfzelz	$⊢ l \in (0 \dots \|N\|) \to l \in ℤ$
53		bccl	$⊢ (\|N\| \in ℕ_{0} \land l \in ℤ) \to (\binom{\|N\|}{l}) \in ℕ_{0}$
54	51 52 53	syl2an	$⊢ (((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}) \in ℕ_{0}$
55		eqid	$⊢ {Base}_{P} = {Base}_{P}$
56	5 55	mgpbas	$⊢ {Base}_{P} = {Base}_{G}$
57	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
58	5	ringmgp	$⊢ P \in Ring \to G \in Mnd$
59	17 57 58	3syl	$⊢ R \in CRing \to G \in Mnd$
60	59	adantl	$⊢ (N \in Fin \land R \in CRing) \to G \in Mnd$
61	60	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 G \in Mnd$
62		elfznn0	$⊢ l \in (0 \dots \|N\|) \to l \in ℕ_{0}$
63	62	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 l \in ℕ_{0}$
64	4 2 55	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
65	18 64	syl	$⊢ (N \in Fin \land R \in CRing) \to X \in {Base}_{P}$
66	65	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 X \in {Base}_{P}$
67	56 6 61 63 66	mulgnn0cld	$⊢ (((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}$
68		eqid	$⊢ Scalar (P) = Scalar (P)$
69		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
70		eqid	$⊢ \cdot_{Scalar (P)} = \cdot_{Scalar (P)}$
71	55 68 14 69 10 70	lmodvsmmulgdi	$⊢ (P \in LMod \land ((\|N\| - l) E I (J M J) \in {Base}_{Scalar (P)} \land (\binom{\|N\|}{l}) \in ℕ_{0} \land l \underset{˙}{\times} X \in {Base}_{P})) \to (\binom{\|N\|}{l}) F (((\|N\| - l) E I (J M J)) \underset{˙}{\cdot} (l \underset{˙}{\times} X)) = ((\binom{\|N\|}{l}) \cdot_{Scalar (P)} ((\|N\| - l) E I (J M J))) \underset{˙}{\cdot} (l \underset{˙}{\times} X)$
72	21 49 54 67 71	syl13anc	$⊢ (((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 (((\|N\| - l) E I (J M J)) \underset{˙}{\cdot} (l \underset{˙}{\times} X)) = ((\binom{\|N\|}{l}) \cdot_{Scalar (P)} ((\|N\| - l) E I (J M J))) \underset{˙}{\cdot} (l \underset{˙}{\times} X)$
73	45	fveq2d	$⊢ (N \in Fin \land R \in CRing) \to \cdot_{R} = \cdot_{Scalar (P)}$
74	15 73	eqtr2id	$⊢ (N \in Fin \land R \in CRing) \to \cdot_{Scalar (P)} = Z$
75	74	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 \cdot_{Scalar (P)} = Z$
76	75	oveqd	$⊢ (((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}) \cdot_{Scalar (P)} ((\|N\| - l) E I (J M J)) = (\binom{\|N\|}{l}) Z ((\|N\| - l) E I (J M J))$
77	76	oveq1d	$⊢ (((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}) \cdot_{Scalar (P)} ((\|N\| - l) E I (J M J))) \underset{˙}{\cdot} (l \underset{˙}{\times} X) = ((\binom{\|N\|}{l}) Z ((\|N\| - l) E I (J M J))) \underset{˙}{\cdot} (l \underset{˙}{\times} X)$
78	72 77	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)) \land l \in (0 \dots \|N\|)) \to (\binom{\|N\|}{l}) F (((\|N\| - l) E I (J M J)) \underset{˙}{\cdot} (l \underset{˙}{\times} X)) = ((\binom{\|N\|}{l}) Z ((\|N\| - l) E I (J M J))) \underset{˙}{\cdot} (l \underset{˙}{\times} X)$
79	78	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 (((\|N\| - l) E I (J M J)) \underset{˙}{\cdot} (l \underset{˙}{\times} X))) = (l \in (0 \dots \|N\|) ⟼ ((\binom{\|N\|}{l}) Z ((\|N\| - l) E I (J M J))) \underset{˙}{\cdot} (l \underset{˙}{\times} X))$
80	79	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 (((\|N\| - l) E I (J M J)) \underset{˙}{\cdot} (l \underset{˙}{\times} X))) = {\sum_{P}}_{l = 0}^{\|N\|} (((\binom{\|N\|}{l}) Z ((\|N\| - l) E I (J M J))) \underset{˙}{\cdot} (l \underset{˙}{\times} X))$
81	16 80	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 C (M) = {\sum_{P}}_{l = 0}^{\|N\|} (((\binom{\|N\|}{l}) Z ((\|N\| - l) E I (J M J))) \underset{˙}{\cdot} (l \underset{˙}{\times} X))$

Metamath Proof Explorer

Theorem chpscmatgsummon

Proof