cpmadugsumfi

Description: The product of the characteristic matrix of a given matrix and its adjunct represented as finite sum. (Contributed by AV, 7-Nov-2019) (Proof shortened by AV, 29-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$
Assertion	cpmadugsumfi	$⊢ (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) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$

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		oveq2	$⊢ J (I) = {\sum_{Y}}_{n = 0}^{s} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n))) \to I \underset{˙}{\times} J (I) = I \underset{˙}{\times} ({\sum_{Y}}_{n = 0}^{s}, ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n))))$
16	13	a1i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to I = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)$
17	16	oveq1d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to I \underset{˙}{\times} ({\sum_{Y}}_{n = 0}^{s}, ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n)))) = ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) \underset{˙}{\times} ({\sum_{Y}}_{n = 0}^{s}, ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n))))$
18		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
19		crngring	$⊢ R \in CRing \to R \in Ring$
20	19	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
21	20	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in Ring)$
22	21	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to (N \in Fin \land R \in Ring)$
23	3 4	pmatring	$⊢ (N \in Fin \land R \in Ring) \to Y \in Ring$
24	22 23	syl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to Y \in Ring$
25	3 4	pmatlmod	$⊢ (N \in Fin \land R \in Ring) \to Y \in LMod$
26	19 25	sylan2	$⊢ (N \in Fin \land R \in CRing) \to Y \in LMod$
27	19	adantl	$⊢ (N \in Fin \land R \in CRing) \to R \in Ring$
28		eqid	$⊢ {Base}_{P} = {Base}_{P}$
29	6 3 28	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
30	27 29	syl	$⊢ (N \in Fin \land R \in CRing) \to X \in {Base}_{P}$
31	3	ply1crng	$⊢ R \in CRing \to P \in CRing$
32	4	matsca2	$⊢ (N \in Fin \land P \in CRing) \to P = Scalar (Y)$
33	31 32	sylan2	$⊢ (N \in Fin \land R \in CRing) \to P = Scalar (Y)$
34	33	fveq2d	$⊢ (N \in Fin \land R \in CRing) \to {Base}_{P} = {Base}_{Scalar (Y)}$
35	30 34	eleqtrd	$⊢ (N \in Fin \land R \in CRing) \to X \in {Base}_{Scalar (Y)}$
36	19 23	sylan2	$⊢ (N \in Fin \land R \in CRing) \to Y \in Ring$
37	18 10	ringidcl	$⊢ Y \in Ring \to \underset{˙}{1} \in {Base}_{Y}$
38	36 37	syl	$⊢ (N \in Fin \land R \in CRing) \to \underset{˙}{1} \in {Base}_{Y}$
39		eqid	$⊢ Scalar (Y) = Scalar (Y)$
40		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
41	18 39 8 40	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}$
42	26 35 38 41	syl3anc	$⊢ (N \in Fin \land R \in CRing) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Y}$
43	42	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Y}$
44	43	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Y}$
45	5 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{Y}$
46	19 45	syl3an2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T (M) \in {Base}_{Y}$
47	46	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to T (M) \in {Base}_{Y}$
48		ringcmn	$⊢ Y \in Ring \to Y \in CMnd$
49	36 48	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in CMnd$
50	49	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in CMnd$
51	50	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to Y \in CMnd$
52		fzfid	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to (0 \dots s) \in Fin$
53	21	ad3antrrr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land n \in (0 \dots s)) \to (N \in Fin \land R \in Ring)$
54		elmapi	$⊢ b \in (B^{(0 \dots s)}) \to b : (0 \dots s) ⟶ B$
55		ffvelcdm	$⊢ (b : (0 \dots s) ⟶ B \land n \in (0 \dots s)) \to b (n) \in B$
56	55	ex	$⊢ b : (0 \dots s) ⟶ B \to (n \in (0 \dots s) \to b (n) \in B)$
57	54 56	syl	$⊢ b \in (B^{(0 \dots s)}) \to (n \in (0 \dots s) \to b (n) \in B)$
58	57	adantl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to (n \in (0 \dots s) \to b (n) \in B)$
59	58	imp	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land n \in (0 \dots s)) \to b (n) \in B$
60		elfznn0	$⊢ n \in (0 \dots s) \to n \in ℕ_{0}$
61	60	adantl	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land n \in (0 \dots s)) \to n \in ℕ_{0}$
62	1 2 5 3 4 18 8 7 6	mat2pmatscmxcl	$⊢ ((N \in Fin \land R \in Ring) \land (b (n) \in B \land n \in ℕ_{0})) \to (n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n)) \in {Base}_{Y}$
63	53 59 61 62	syl12anc	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land n \in (0 \dots s)) \to (n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n)) \in {Base}_{Y}$
64	63	ralrimiva	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to \forall n \in (0 \dots s) (n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n)) \in {Base}_{Y}$
65	18 51 52 64	gsummptcl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to {\sum_{Y}}_{n = 0}^{s} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n))) \in {Base}_{Y}$
66	18 9 12 24 44 47 65	ringsubdir	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) \underset{˙}{\times} ({\sum_{Y}}_{n = 0}^{s}, ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n)))) = ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ({\sum_{Y}}_{n = 0}^{s}, ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n))))) \underset{˙}{-} (T (M) \underset{˙}{\times} ({\sum_{Y}}_{n = 0}^{s}, ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n)))))$
67		oveq1	$⊢ n = i \to n \underset{˙}{\times} X = i \underset{˙}{\times} X$
68		2fveq3	$⊢ n = i \to T (b (n)) = T (b (i))$
69	67 68	oveq12d	$⊢ n = i \to (n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n)) = (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))$
70	69	cbvmptv	$⊢ (n \in (0 \dots s) ⟼ (n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n))) = (i \in (0 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))$
71	70	oveq2i	$⊢ {\sum_{Y}}_{n = 0}^{s} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n))) = {\sum_{Y}}_{i = 0}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))$
72	71	oveq2i	$⊢ (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ({\sum_{Y}}_{n = 0}^{s}, ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n)))) = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))$
73	71	oveq2i	$⊢ T (M) \underset{˙}{\times} ({\sum_{Y}}_{n = 0}^{s}, ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n)))) = T (M) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))$
74	72 73	oveq12i	$⊢ ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ({\sum_{Y}}_{n = 0}^{s}, ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n))))) \underset{˙}{-} (T (M) \underset{˙}{\times} ({\sum_{Y}}_{n = 0}^{s}, ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n))))) = ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))) \underset{˙}{-} (T (M) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))))$
75	1 2 3 4 5 6 7 8 9 10 11 12	cpmadugsumlemF	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))) \underset{˙}{-} (T (M) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
76	75	anassrs	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))) \underset{˙}{-} (T (M) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
77	74 76	eqtrid	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ({\sum_{Y}}_{n = 0}^{s}, ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n))))) \underset{˙}{-} (T (M) \underset{˙}{\times} ({\sum_{Y}}_{n = 0}^{s}, ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n))))) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
78	17 66 77	3eqtrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to I \underset{˙}{\times} ({\sum_{Y}}_{n = 0}^{s}, ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n)))) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
79	15 78	sylan9eqr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land J (I) = {\sum_{Y}}_{n = 0}^{s} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n)))) \to I \underset{˙}{\times} J (I) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
80	4 14 18	maduf	$⊢ P \in CRing \to J : {Base}_{Y} ⟶ {Base}_{Y}$
81	31 80	syl	$⊢ R \in CRing \to J : {Base}_{Y} ⟶ {Base}_{Y}$
82	81	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to J : {Base}_{Y} ⟶ {Base}_{Y}$
83	1 2 3 4 6 5 12 8 10 13	chmatcl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to I \in {Base}_{Y}$
84	19 83	syl3an2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to I \in {Base}_{Y}$
85	82 84	ffvelcdmd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to J (I) \in {Base}_{Y}$
86	3 4 18 8 7 6 5 1 2	pmatcollpw3fi1	$⊢ (N \in Fin \land R \in CRing \land J (I) \in {Base}_{Y}) \to \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) J (I) = {\sum_{Y}}_{n = 0}^{s} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n)))$
87	85 86	syld3an3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) J (I) = {\sum_{Y}}_{n = 0}^{s} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (n)))$
88	79 87	reximddv2	$⊢ (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) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$

Metamath Proof Explorer

Theorem cpmadugsumfi

Proof