cpmidgsum2

Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as another group sum. (Contributed by AV, 10-Nov-2019)

	Ref	Expression
Hypotheses	cpmadugsum.a	$⊢ A = N Mat R$
	cpmadugsum.b	$⊢ B = {Base}_{A}$
	cpmadugsum.p	$⊢ P = {Poly}_{1} (R)$
	cpmadugsum.y	$⊢ Y = N Mat P$
	cpmadugsum.t	$⊢ T = N matToPolyMat R$
	cpmadugsum.x	$⊢ X = {var}_{1} (R)$
	cpmadugsum.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	cpmadugsum.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	cpmadugsum.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
	cpmadugsum.1	$⊢ \underset{˙}{1} = 1_{Y}$
	cpmadugsum.g	$⊢ \underset{˙}{+} = +_{Y}$
	cpmadugsum.s	$⊢ \underset{˙}{-} = -_{Y}$
	cpmadugsum.i	$⊢ I = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)$
	cpmadugsum.j	$⊢ J = N maAdju P$
	cpmadugsum.0	$⊢ \underset{˙}{0} = 0_{Y}$
	cpmadugsum.g2	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))), if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))))))$
	cpmidgsum2.c	$⊢ C = N CharPlyMat R$
	cpmidgsum2.k	$⊢ K = C (M)$
	cpmidgsum2.h	$⊢ H = K \underset{˙}{\cdot} \underset{˙}{1}$
Assertion	cpmidgsum2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) H = \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))$

Proof

Step	Hyp	Ref	Expression
1		cpmadugsum.a	$⊢ A = N Mat R$
2		cpmadugsum.b	$⊢ B = {Base}_{A}$
3		cpmadugsum.p	$⊢ P = {Poly}_{1} (R)$
4		cpmadugsum.y	$⊢ Y = N Mat P$
5		cpmadugsum.t	$⊢ T = N matToPolyMat R$
6		cpmadugsum.x	$⊢ X = {var}_{1} (R)$
7		cpmadugsum.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
8		cpmadugsum.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
9		cpmadugsum.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
10		cpmadugsum.1	$⊢ \underset{˙}{1} = 1_{Y}$
11		cpmadugsum.g	$⊢ \underset{˙}{+} = +_{Y}$
12		cpmadugsum.s	$⊢ \underset{˙}{-} = -_{Y}$
13		cpmadugsum.i	$⊢ I = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)$
14		cpmadugsum.j	$⊢ J = N maAdju P$
15		cpmadugsum.0	$⊢ \underset{˙}{0} = 0_{Y}$
16		cpmadugsum.g2	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))), if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))))))$
17		cpmidgsum2.c	$⊢ C = N CharPlyMat R$
18		cpmidgsum2.k	$⊢ K = C (M)$
19		cpmidgsum2.h	$⊢ H = K \underset{˙}{\cdot} \underset{˙}{1}$
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	cpmadugsum	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) I \underset{˙}{\times} J (I) = \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))$
21		crngring	$⊢ R \in CRing \to R \in Ring$
22	21	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
23	22	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in Ring)$
24	3 4	pmatring	$⊢ (N \in Fin \land R \in Ring) \to Y \in Ring$
25		ringgrp	$⊢ Y \in Ring \to Y \in Grp$
26	23 24 25	3syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Grp$
27	3 4	pmatlmod	$⊢ (N \in Fin \land R \in Ring) \to Y \in LMod$
28	21 27	sylan2	$⊢ (N \in Fin \land R \in CRing) \to Y \in LMod$
29	21	adantl	$⊢ (N \in Fin \land R \in CRing) \to R \in Ring$
30		eqid	$⊢ {Base}_{P} = {Base}_{P}$
31	6 3 30	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
32	29 31	syl	$⊢ (N \in Fin \land R \in CRing) \to X \in {Base}_{P}$
33	3	ply1crng	$⊢ R \in CRing \to P \in CRing$
34	4	matsca2	$⊢ (N \in Fin \land P \in CRing) \to P = Scalar (Y)$
35	33 34	sylan2	$⊢ (N \in Fin \land R \in CRing) \to P = Scalar (Y)$
36	35	fveq2d	$⊢ (N \in Fin \land R \in CRing) \to {Base}_{P} = {Base}_{Scalar (Y)}$
37	32 36	eleqtrd	$⊢ (N \in Fin \land R \in CRing) \to X \in {Base}_{Scalar (Y)}$
38		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
39	38 10	ringidcl	$⊢ Y \in Ring \to \underset{˙}{1} \in {Base}_{Y}$
40	22 24 39	3syl	$⊢ (N \in Fin \land R \in CRing) \to \underset{˙}{1} \in {Base}_{Y}$
41		eqid	$⊢ Scalar (Y) = Scalar (Y)$
42		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
43	38 41 8 42	lmodvscl	$⊢ (Y \in LMod \land X \in {Base}_{Scalar (Y)} \land \underset{˙}{1} \in {Base}_{Y}) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Y}$
44	28 37 40 43	syl3anc	$⊢ (N \in Fin \land R \in CRing) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Y}$
45	44	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Y}$
46	5 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{Y}$
47	21 46	syl3an2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T (M) \in {Base}_{Y}$
48	38 12	grpsubcl	$⊢ (Y \in Grp \land X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Y} \land T (M) \in {Base}_{Y}) \to (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M) \in {Base}_{Y}$
49	26 45 47 48	syl3anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M) \in {Base}_{Y}$
50	33	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P \in CRing$
51		eqid	$⊢ N maDet P = N maDet P$
52	4 38 14 51 10 9 8	madurid	$⊢ ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M) \in {Base}_{Y} \land P \in CRing) \to ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) \underset{˙}{\times} J ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) = (N maDet P) ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) \underset{˙}{\cdot} \underset{˙}{1}$
53	49 50 52	syl2anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) \underset{˙}{\times} J ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) = (N maDet P) ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) \underset{˙}{\cdot} \underset{˙}{1}$
54		id	$⊢ I = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M) \to I = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)$
55		fveq2	$⊢ I = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M) \to J (I) = J ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M))$
56	54 55	oveq12d	$⊢ I = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M) \to I \underset{˙}{\times} J (I) = ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) \underset{˙}{\times} J ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M))$
57	13 56	mp1i	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to I \underset{˙}{\times} J (I) = ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) \underset{˙}{\times} J ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M))$
58	17 1 2 3 4 51 12 6 8 5 10	chpmatval	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) = (N maDet P) ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M))$
59	18 58	eqtrid	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to K = (N maDet P) ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M))$
60	59	oveq1d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to K \underset{˙}{\cdot} \underset{˙}{1} = (N maDet P) ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) \underset{˙}{\cdot} \underset{˙}{1}$
61	19 60	eqtrid	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to H = (N maDet P) ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) \underset{˙}{\cdot} \underset{˙}{1}$
62	53 57 61	3eqtr4rd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to H = I \underset{˙}{\times} J (I)$
63	62	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land I \underset{˙}{\times} J (I) = \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \to H = I \underset{˙}{\times} J (I)$
64		simpr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land I \underset{˙}{\times} J (I) = \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \to I \underset{˙}{\times} J (I) = \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))$
65	63 64	eqtrd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land I \underset{˙}{\times} J (I) = \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \to H = \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))$
66	65	ex	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (I \underset{˙}{\times} J (I) = \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) \to H = \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)))$
67	66	reximdv	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (\exists b \in (B^{(0 \dots s)}) I \underset{˙}{\times} J (I) = \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) \to \exists b \in (B^{(0 \dots s)}) H = \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)))$
68	67	reximdv	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (\exists s \in ℕ \exists b \in (B^{(0 \dots s)}) I \underset{˙}{\times} J (I) = \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) \to \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) H = \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)))$
69	20 68	mpd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) H = \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))$

Metamath Proof Explorer

Theorem cpmidgsum2

Proof