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	11	ringmgp	$⊢ R \in Ring \to H \in Mnd$
23	18 22	syl	$⊢ (N \in Fin \land R \in CRing) \to H \in Mnd$
24	23	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$
25		fznn0sub	$⊢ l \in (0 \dots \|N\|) \to \|N\| - l \in ℕ_{0}$
26	25	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}$
27		ringgrp	$⊢ R \in Ring \to R \in Grp$
28	17 27	syl	$⊢ R \in CRing \to R \in Grp$
29	28	adantl	$⊢ (N \in Fin \land R \in CRing) \to R \in Grp$
30		simp2	$⊢ (M \in D \land J \in N \land \forall n \in N n M n = J M J) \to J \in N$
31		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}$
32	31 7	eleq2s	$⊢ M \in D \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 M \in {Base}_{A}$
34	30 30 33	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})$
35	34	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})$
36		eqid	$⊢ {Base}_{R} = {Base}_{R}$
37	3 36	matecl	$⊢ (J \in N \land J \in N \land M \in {Base}_{A}) \to J M J \in {Base}_{R}$
38	35 37	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}$
39	36 13	grpinvcl	$⊢ (R \in Grp \land J M J \in {Base}_{R}) \to I (J M J) \in {Base}_{R}$
40	29 38 39	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}$
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)) \land l \in (0 \dots \|N\|)) \to I (J M J) \in {Base}_{R}$
42	11 36	mgpbas	$⊢ {Base}_{R} = {Base}_{H}$
43	42 12	mulgnn0cl	$⊢ (H \in Mnd \land \|N\| - l \in ℕ_{0} \land I (J M J) \in {Base}_{R}) \to (\|N\| - l) E I (J M J) \in {Base}_{R}$
44	24 26 41 43	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}_{R}$
45	2	ply1sca	$⊢ R \in CRing \to R = Scalar (P)$
46	45	adantl	$⊢ (N \in Fin \land R \in CRing) \to R = Scalar (P)$
47	46	eqcomd	$⊢ (N \in Fin \land R \in CRing) \to Scalar (P) = R$
48	47	fveq2d	$⊢ (N \in Fin \land R \in CRing) \to {Base}_{Scalar (P)} = {Base}_{R}$
49	48	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}$
50	44 49	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)}$
51		hashcl	$⊢ N \in Fin \to \|N\| \in ℕ_{0}$
52	51	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}$
53		elfzelz	$⊢ l \in (0 \dots \|N\|) \to l \in ℤ$
54		bccl	$⊢ (\|N\| \in ℕ_{0} \land l \in ℤ) \to (\binom{\|N\|}{l}) \in ℕ_{0}$
55	52 53 54	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}$
56	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
57	5	ringmgp	$⊢ P \in Ring \to G \in Mnd$
58	17 56 57	3syl	$⊢ R \in CRing \to G \in Mnd$
59	58	adantl	$⊢ (N \in Fin \land R \in CRing) \to G \in Mnd$
60	59	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$
61		elfznn0	$⊢ l \in (0 \dots \|N\|) \to l \in ℕ_{0}$
62	61	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}$
63		eqid	$⊢ {Base}_{P} = {Base}_{P}$
64	4 2 63	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	5 63	mgpbas	$⊢ {Base}_{P} = {Base}_{G}$
68	67 6	mulgnn0cl	$⊢ (G \in Mnd \land l \in ℕ_{0} \land X \in {Base}_{P}) \to l \underset{˙}{\times} X \in {Base}_{P}$
69	60 62 66 68	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 l \underset{˙}{\times} X \in {Base}_{P}$
70		eqid	$⊢ Scalar (P) = Scalar (P)$
71		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
72		eqid	$⊢ \cdot_{Scalar (P)} = \cdot_{Scalar (P)}$
73	63 70 14 71 10 72	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)$
74	21 50 55 69 73	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)$
75	46	fveq2d	$⊢ (N \in Fin \land R \in CRing) \to \cdot_{R} = \cdot_{Scalar (P)}$
76	15 75	syl5req	$⊢ (N \in Fin \land R \in CRing) \to \cdot_{Scalar (P)} = Z$
77	76	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$
78	77	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))$
79	78	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)$
80	74 79	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)$
81	80	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))$
82	81	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))$
83	16 82	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