cayleyhamilton1

Description: The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation", or, in other words, a matrix over a commutative ring "inserted" into its characteristic polynomial results in zero. In this variant of cayleyhamilton , the meaning of "inserted" is made more transparent: If the characteristic polynomial is a polynomial with coefficients ( Fn ) , then a matrix over a commutative ring "inserted" into its characteristic polynomial is the sum of these coefficients multiplied with the corresponding power of the matrix. (Contributed by AV, 25-Nov-2019)

	Ref	Expression
Hypotheses	cayleyhamilton.a	$⊢ A = N Mat R$
	cayleyhamilton.b	$⊢ B = {Base}_{A}$
	cayleyhamilton.0	$⊢ \underset{˙}{0} = 0_{A}$
	cayleyhamilton.c	$⊢ C = N CharPlyMat R$
	cayleyhamilton.k	$⊢ K = {coe}_{1} (C (M))$
	cayleyhamilton.m	$⊢ \underset{˙}{*} = \cdot_{A}$
	cayleyhamilton.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{A}}$
	cayleyhamilton1.l	$⊢ L = {Base}_{R}$
	cayleyhamilton1.x	$⊢ X = {var}_{1} (R)$
	cayleyhamilton1.p	$⊢ P = {Poly}_{1} (R)$
	cayleyhamilton1.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	cayleyhamilton1.e	$⊢ E = \cdot_{{mulGrp}_{P}}$
	cayleyhamilton1.z	$⊢ Z = 0_{R}$
Assertion	cayleyhamilton1	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to (C (M) = \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X)) \to \underset{n \in ℕ_{0}}{\sum_{A}} (F (n) \underset{˙}{*} (n \underset{˙}{\times} M)) = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		cayleyhamilton.a	$⊢ A = N Mat R$
2		cayleyhamilton.b	$⊢ B = {Base}_{A}$
3		cayleyhamilton.0	$⊢ \underset{˙}{0} = 0_{A}$
4		cayleyhamilton.c	$⊢ C = N CharPlyMat R$
5		cayleyhamilton.k	$⊢ K = {coe}_{1} (C (M))$
6		cayleyhamilton.m	$⊢ \underset{˙}{*} = \cdot_{A}$
7		cayleyhamilton.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{A}}$
8		cayleyhamilton1.l	$⊢ L = {Base}_{R}$
9		cayleyhamilton1.x	$⊢ X = {var}_{1} (R)$
10		cayleyhamilton1.p	$⊢ P = {Poly}_{1} (R)$
11		cayleyhamilton1.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
12		cayleyhamilton1.e	$⊢ E = \cdot_{{mulGrp}_{P}}$
13		cayleyhamilton1.z	$⊢ Z = 0_{R}$
14	1 2 3 4 5 6 7	cayleyhamilton	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{*} (n \underset{˙}{\times} M)) = \underset{˙}{0}$
15	14	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{*} (n \underset{˙}{\times} M)) = \underset{˙}{0}$
16		nfv	$⊢ Ⅎ n ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F)))$
17		nfcv	$⊢ \underline{Ⅎ} n P$
18		nfcv	$⊢ \underline{Ⅎ} n Σ_{𝑔}$
19		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ_{0} ⟼ F (n) \underset{˙}{\cdot} (n E X))$
20	17 18 19	nfov	$⊢ \underline{Ⅎ} n (\underset{n \in ℕ_{0}}{\sum_{P}}, (F (n) \underset{˙}{\cdot} (n E X)))$
21	20	nfeq2	$⊢ Ⅎ n C (M) = \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X))$
22	16 21	nfan	$⊢ Ⅎ n (((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \land C (M) = \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X)))$
23		crngring	$⊢ R \in CRing \to R \in Ring$
24	23	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
25	24	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to R \in Ring$
26		eqid	$⊢ {Base}_{P} = {Base}_{P}$
27	4 1 2 10 26	chpmatply1	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) \in {Base}_{P}$
28	27	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to C (M) \in {Base}_{P}$
29		eqid	$⊢ 0_{R} = 0_{R}$
30		elmapi	$⊢ F \in (L^{ℕ_{0}}) \to F : ℕ_{0} ⟶ L$
31		ffvelcdm	$⊢ (F : ℕ_{0} ⟶ L \land n \in ℕ_{0}) \to F (n) \in L$
32	31	ralrimiva	$⊢ F : ℕ_{0} ⟶ L \to \forall n \in ℕ_{0} F (n) \in L$
33	30 32	syl	$⊢ F \in (L^{ℕ_{0}}) \to \forall n \in ℕ_{0} F (n) \in L$
34	33	ad2antrl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to \forall n \in ℕ_{0} F (n) \in L$
35	30	feqmptd	$⊢ F \in (L^{ℕ_{0}}) \to F = (n \in ℕ_{0} ⟼ F (n))$
36	13	a1i	$⊢ F \in (L^{ℕ_{0}}) \to Z = 0_{R}$
37	35 36	breq12d	$⊢ F \in (L^{ℕ_{0}}) \to ({finSupp}_{Z} (F) \leftrightarrow {finSupp}_{0_{R}} ((n \in ℕ_{0} ⟼ F (n))))$
38	37	biimpa	$⊢ (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F)) \to {finSupp}_{0_{R}} ((n \in ℕ_{0} ⟼ F (n)))$
39	38	adantl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to {finSupp}_{0_{R}} ((n \in ℕ_{0} ⟼ F (n)))$
40	10 26 9 12 25 8 11 29 34 39	gsumsmonply1	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X)) \in {Base}_{P}$
41		fveq2	$⊢ i = n \to F (i) = F (n)$
42		oveq1	$⊢ i = n \to i E X = n E X$
43	41 42	oveq12d	$⊢ i = n \to F (i) \underset{˙}{\cdot} (i E X) = F (n) \underset{˙}{\cdot} (n E X)$
44	43	cbvmptv	$⊢ (i \in ℕ_{0} ⟼ F (i) \underset{˙}{\cdot} (i E X)) = (n \in ℕ_{0} ⟼ F (n) \underset{˙}{\cdot} (n E X))$
45	44	oveq2i	$⊢ \underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X)) = \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X))$
46	45	fveq2i	$⊢ {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) = {coe}_{1} (\underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X)))$
47	10 26 5 46	ply1coe1eq	$⊢ (R \in Ring \land C (M) \in {Base}_{P} \land \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X)) \in {Base}_{P}) \to (\forall m \in ℕ_{0} K (m) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (m) \leftrightarrow C (M) = \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X)))$
48	25 28 40 47	syl3anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to (\forall m \in ℕ_{0} K (m) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (m) \leftrightarrow C (M) = \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X)))$
49		fveq2	$⊢ m = n \to K (m) = K (n)$
50		fveq2	$⊢ m = n \to {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (m) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (n)$
51	49 50	eqeq12d	$⊢ m = n \to (K (m) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (m) \leftrightarrow K (n) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (n))$
52	51	rspcva	$⊢ (n \in ℕ_{0} \land \forall m \in ℕ_{0} K (m) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (m)) \to K (n) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (n)$
53		simpl	$⊢ (K (n) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (n) \land (n \in ℕ_{0} \land ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))))) \to K (n) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (n)$
54	24	ad2antrl	$⊢ (n \in ℕ_{0} \land ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F)))) \to R \in Ring$
55		ffvelcdm	$⊢ (F : ℕ_{0} ⟶ L \land i \in ℕ_{0}) \to F (i) \in L$
56	55	ralrimiva	$⊢ F : ℕ_{0} ⟶ L \to \forall i \in ℕ_{0} F (i) \in L$
57	30 56	syl	$⊢ F \in (L^{ℕ_{0}}) \to \forall i \in ℕ_{0} F (i) \in L$
58	57	ad2antrl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to \forall i \in ℕ_{0} F (i) \in L$
59	58	adantl	$⊢ (n \in ℕ_{0} \land ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F)))) \to \forall i \in ℕ_{0} F (i) \in L$
60	30	feqmptd	$⊢ F \in (L^{ℕ_{0}}) \to F = (i \in ℕ_{0} ⟼ F (i))$
61	60	breq1d	$⊢ F \in (L^{ℕ_{0}}) \to ({finSupp}_{Z} (F) \leftrightarrow {finSupp}_{Z} ((i \in ℕ_{0} ⟼ F (i))))$
62	61	biimpa	$⊢ (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F)) \to {finSupp}_{Z} ((i \in ℕ_{0} ⟼ F (i)))$
63	62	adantl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to {finSupp}_{Z} ((i \in ℕ_{0} ⟼ F (i)))$
64	63	adantl	$⊢ (n \in ℕ_{0} \land ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F)))) \to {finSupp}_{Z} ((i \in ℕ_{0} ⟼ F (i)))$
65		simpl	$⊢ (n \in ℕ_{0} \land ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F)))) \to n \in ℕ_{0}$
66	10 26 9 12 54 8 11 13 59 64 65	gsummoncoe1	$⊢ (n \in ℕ_{0} \land ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F)))) \to {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (n) = ⦋ n / i ⦌ F (i)$
67		csbfv	$⊢ ⦋ n / i ⦌ F (i) = F (n)$
68	66 67	eqtrdi	$⊢ (n \in ℕ_{0} \land ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F)))) \to {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (n) = F (n)$
69	68	adantl	$⊢ (K (n) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (n) \land (n \in ℕ_{0} \land ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))))) \to {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (n) = F (n)$
70	53 69	eqtrd	$⊢ (K (n) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (n) \land (n \in ℕ_{0} \land ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))))) \to K (n) = F (n)$
71	70	exp32	$⊢ K (n) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (n) \to (n \in ℕ_{0} \to (((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to K (n) = F (n)))$
72	71	com12	$⊢ n \in ℕ_{0} \to (K (n) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (n) \to (((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to K (n) = F (n)))$
73	72	adantr	$⊢ (n \in ℕ_{0} \land \forall m \in ℕ_{0} K (m) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (m)) \to (K (n) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (n) \to (((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to K (n) = F (n)))$
74	52 73	mpd	$⊢ (n \in ℕ_{0} \land \forall m \in ℕ_{0} K (m) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (m)) \to (((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to K (n) = F (n))$
75	74	com12	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to ((n \in ℕ_{0} \land \forall m \in ℕ_{0} K (m) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (m)) \to K (n) = F (n))$
76	75	expcomd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to (\forall m \in ℕ_{0} K (m) = {coe}_{1} (\underset{i \in ℕ_{0}}{\sum_{P}} (F (i) \underset{˙}{\cdot} (i E X))) (m) \to (n \in ℕ_{0} \to K (n) = F (n)))$
77	48 76	sylbird	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to (C (M) = \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X)) \to (n \in ℕ_{0} \to K (n) = F (n)))$
78	77	imp31	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \land C (M) = \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X))) \land n \in ℕ_{0}) \to K (n) = F (n)$
79	78	oveq1d	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \land C (M) = \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X))) \land n \in ℕ_{0}) \to K (n) \underset{˙}{} (n \underset{˙}{\times} M) = F (n) \underset{˙}{} (n \underset{˙}{\times} M)$
80	22 79	mpteq2da	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \land C (M) = \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X))) \to (n \in ℕ_{0} ⟼ K (n) \underset{˙}{} (n \underset{˙}{\times} M)) = (n \in ℕ_{0} ⟼ F (n) \underset{˙}{} (n \underset{˙}{\times} M))$
81	80	oveq2d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \land C (M) = \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X))) \to \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{n \in ℕ_{0}}{\sum_{A}} (F (n) \underset{˙}{} (n \underset{˙}{\times} M))$
82	81	eqeq1d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \land C (M) = \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X))) \to (\underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{˙}{0} \leftrightarrow \underset{n \in ℕ_{0}}{\sum_{A}} (F (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{˙}{0})$
83	82	biimpd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \land C (M) = \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X))) \to (\underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{˙}{0} \to \underset{n \in ℕ_{0}}{\sum_{A}} (F (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{˙}{0})$
84	83	ex	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to (C (M) = \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X)) \to (\underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{˙}{0} \to \underset{n \in ℕ_{0}}{\sum_{A}} (F (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{˙}{0}))$
85	15 84	mpid	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (F \in (L^{ℕ_{0}}) \land {finSupp}_{Z} (F))) \to (C (M) = \underset{n \in ℕ_{0}}{\sum_{P}} (F (n) \underset{˙}{\cdot} (n E X)) \to \underset{n \in ℕ_{0}}{\sum_{A}} (F (n) \underset{˙}{*} (n \underset{˙}{\times} M)) = \underset{˙}{0})$

Metamath Proof Explorer

Theorem cayleyhamilton1

Proof