cayhamlem4

Description: Lemma for cayleyhamilton . (Contributed by AV, 25-Nov-2019) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	chcoeffeq.a	$⊢ A = N Mat R$
	chcoeffeq.b	$⊢ B = {Base}_{A}$
	chcoeffeq.p	$⊢ P = {Poly}_{1} (R)$
	chcoeffeq.y	$⊢ Y = N Mat P$
	chcoeffeq.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
	chcoeffeq.s	$⊢ \underset{˙}{-} = -_{Y}$
	chcoeffeq.0	$⊢ \underset{˙}{0} = 0_{Y}$
	chcoeffeq.t	$⊢ T = N matToPolyMat R$
	chcoeffeq.c	$⊢ C = N CharPlyMat R$
	chcoeffeq.k	$⊢ K = C (M)$
	chcoeffeq.g	$⊢ 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)))))))$
	chcoeffeq.w	$⊢ W = {Base}_{Y}$
	chcoeffeq.1	$⊢ \underset{˙}{1} = 1_{A}$
	chcoeffeq.m	$⊢ \underset{˙}{*} = \cdot_{A}$
	chcoeffeq.u	$⊢ U = N cPolyMatToMat R$
	cayhamlem.e1	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{A}}$
	cayhamlem.e2	$⊢ E = \cdot_{{mulGrp}_{Y}}$
Assertion	cayhamlem4	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (K) (n) \underset{˙}{*} (n \underset{˙}{\times} M)) = U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n)))$

Proof

Step	Hyp	Ref	Expression
1		chcoeffeq.a	$⊢ A = N Mat R$
2		chcoeffeq.b	$⊢ B = {Base}_{A}$
3		chcoeffeq.p	$⊢ P = {Poly}_{1} (R)$
4		chcoeffeq.y	$⊢ Y = N Mat P$
5		chcoeffeq.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
6		chcoeffeq.s	$⊢ \underset{˙}{-} = -_{Y}$
7		chcoeffeq.0	$⊢ \underset{˙}{0} = 0_{Y}$
8		chcoeffeq.t	$⊢ T = N matToPolyMat R$
9		chcoeffeq.c	$⊢ C = N CharPlyMat R$
10		chcoeffeq.k	$⊢ K = C (M)$
11		chcoeffeq.g	$⊢ 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)))))))$
12		chcoeffeq.w	$⊢ W = {Base}_{Y}$
13		chcoeffeq.1	$⊢ \underset{˙}{1} = 1_{A}$
14		chcoeffeq.m	$⊢ \underset{˙}{*} = \cdot_{A}$
15		chcoeffeq.u	$⊢ U = N cPolyMatToMat R$
16		cayhamlem.e1	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{A}}$
17		cayhamlem.e2	$⊢ E = \cdot_{{mulGrp}_{Y}}$
18		id	$⊢ \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) \to \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \cdot_{A} U (G (n)))$
19		simp1	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to N \in Fin$
20	19	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$
21		crngring	$⊢ R \in CRing \to R \in Ring$
22	21	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
23	22	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to R \in Ring$
24		eqid	$⊢ 0_{A} = 0_{A}$
25	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
26	21 25	sylan2	$⊢ (N \in Fin \land R \in CRing) \to A \in Ring$
27		ringcmn	$⊢ A \in Ring \to A \in CMnd$
28	26 27	syl	$⊢ (N \in Fin \land R \in CRing) \to A \in CMnd$
29	28	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to A \in CMnd$
30	29	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to A \in CMnd$
31		nn0ex	$⊢ ℕ_{0} \in V$
32	31	a1i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to ℕ_{0} \in V$
33	20 23 25	syl2anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to A \in Ring$
34	33	adantr	$⊢ ((((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}) \to A \in Ring$
35		eqid	$⊢ {mulGrp}_{A} = {mulGrp}_{A}$
36	35 2	mgpbas	$⊢ B = {Base}_{{mulGrp}_{A}}$
37	19 22 25	syl2anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to A \in Ring$
38	35	ringmgp	$⊢ A \in Ring \to {mulGrp}_{A} \in Mnd$
39	37 38	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{A} \in Mnd$
40	39	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}) \to {mulGrp}_{A} \in Mnd$
41		simpr	$⊢ ((((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}) \to n \in ℕ_{0}$
42		simpll3	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to M \in B$
43	42	adantr	$⊢ ((((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}) \to M \in B$
44	36 16 40 41 43	mulgnn0cld	$⊢ ((((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}) \to n \underset{˙}{\times} M \in B$
45		eqid	$⊢ N ConstPolyMat R = N ConstPolyMat R$
46	1 2 45 15	cpm2mf	$⊢ (N \in Fin \land R \in Ring) \to U : N ConstPolyMat R ⟶ B$
47	19 22 46	syl2anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to U : N ConstPolyMat R ⟶ B$
48	47	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}) \to U : N ConstPolyMat R ⟶ B$
49		simplr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to s \in ℕ$
50		simpr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to b \in (B^{(0 \dots s)})$
51	1 2 3 4 5 6 7 8 11 45	chfacfisfcpmat	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to G : ℕ_{0} ⟶ N ConstPolyMat R$
52	20 23 42 49 50 51	syl32anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to G : ℕ_{0} ⟶ N ConstPolyMat R$
53	52	ffvelcdmda	$⊢ ((((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}) \to G (n) \in (N ConstPolyMat R)$
54	48 53	ffvelcdmd	$⊢ ((((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}) \to U (G (n)) \in B$
55		eqid	$⊢ \cdot_{A} = \cdot_{A}$
56	2 55	ringcl	$⊢ (A \in Ring \land n \underset{˙}{\times} M \in B \land U (G (n)) \in B) \to (n \underset{˙}{\times} M) \cdot_{A} U (G (n)) \in B$
57	34 44 54 56	syl3anc	$⊢ ((((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}) \to (n \underset{˙}{\times} M) \cdot_{A} U (G (n)) \in B$
58	57	fmpttd	$⊢ (((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} ⟼ (n \underset{˙}{\times} M) \cdot_{A} U (G (n))) : ℕ_{0} ⟶ B$
59		fvexd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to 0_{A} \in V$
60		ovexd	$⊢ ((((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}) \to (n \underset{˙}{\times} M) \cdot_{A} U (G (n)) \in V$
61	1 2 3 4 5 6 7 8 11	chfacffsupp	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to {finSupp}_{0_{Y}} (G)$
62	61	anassrs	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to {finSupp}_{0_{Y}} (G)$
63		ovex	$⊢ N ConstPolyMat R \in V$
64	63 31	pm3.2i	$⊢ (N ConstPolyMat R \in V \land ℕ_{0} \in V)$
65		elmapg	$⊢ (N ConstPolyMat R \in V \land ℕ_{0} \in V) \to (G \in ({(N ConstPolyMat R)}^{ℕ_{0}}) \leftrightarrow G : ℕ_{0} ⟶ N ConstPolyMat R)$
66	64 65	mp1i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to (G \in ({(N ConstPolyMat R)}^{ℕ_{0}}) \leftrightarrow G : ℕ_{0} ⟶ N ConstPolyMat R)$
67	52 66	mpbird	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to G \in ({(N ConstPolyMat R)}^{ℕ_{0}})$
68		fvex	$⊢ 0_{Y} \in V$
69		fsuppmapnn0ub	$⊢ (G \in ({(N ConstPolyMat R)}^{ℕ_{0}}) \land 0_{Y} \in V) \to ({finSupp}_{0_{Y}} (G) \to \exists w \in ℕ_{0} \forall z \in ℕ_{0} (w < z \to G (z) = 0_{Y}))$
70	67 68 69	sylancl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to ({finSupp}_{0_{Y}} (G) \to \exists w \in ℕ_{0} \forall z \in ℕ_{0} (w < z \to G (z) = 0_{Y}))$
71		csbov12g	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = ⦋ z / n ⦌ (n \underset{˙}{\times} M) \cdot_{A} ⦋ z / n ⦌ U (G (n))$
72		csbov1g	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ (n \underset{˙}{\times} M) = ⦋ z / n ⦌ n \underset{˙}{\times} M$
73		csbvarg	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ n = z$
74	73	oveq1d	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ n \underset{˙}{\times} M = z \underset{˙}{\times} M$
75	72 74	eqtrd	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ (n \underset{˙}{\times} M) = z \underset{˙}{\times} M$
76		csbfv2g	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ U (G (n)) = U (⦋ z / n ⦌ G (n))$
77		csbfv	$⊢ ⦋ z / n ⦌ G (n) = G (z)$
78	77	a1i	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ G (n) = G (z)$
79	78	fveq2d	$⊢ z \in ℕ_{0} \to U (⦋ z / n ⦌ G (n)) = U (G (z))$
80	76 79	eqtrd	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ U (G (n)) = U (G (z))$
81	75 80	oveq12d	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ (n \underset{˙}{\times} M) \cdot_{A} ⦋ z / n ⦌ U (G (n)) = (z \underset{˙}{\times} M) \cdot_{A} U (G (z))$
82	71 81	eqtrd	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = (z \underset{˙}{\times} M) \cdot_{A} U (G (z))$
83	82	ad2antlr	$⊢ (((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land z \in ℕ_{0}) \land G (z) = 0_{Y}) \to ⦋ z / n ⦌ ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = (z \underset{˙}{\times} M) \cdot_{A} U (G (z))$
84		fveq2	$⊢ G (z) = 0_{Y} \to U (G (z)) = U (0_{Y})$
85	19 22	jca	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in Ring)$
86	85	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \to (N \in Fin \land R \in Ring)$
87		eqid	$⊢ 0_{Y} = 0_{Y}$
88	1 15 3 4 24 87	m2cpminv0	$⊢ (N \in Fin \land R \in Ring) \to U (0_{Y}) = 0_{A}$
89	86 88	syl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \to U (0_{Y}) = 0_{A}$
90	89	ad2antrr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land z \in ℕ_{0}) \to U (0_{Y}) = 0_{A}$
91	84 90	sylan9eqr	$⊢ (((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land z \in ℕ_{0}) \land G (z) = 0_{Y}) \to U (G (z)) = 0_{A}$
92	91	oveq2d	$⊢ (((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land z \in ℕ_{0}) \land G (z) = 0_{Y}) \to (z \underset{˙}{\times} M) \cdot_{A} U (G (z)) = (z \underset{˙}{\times} M) \cdot_{A} 0_{A}$
93	33	adantr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land z \in ℕ_{0}) \to A \in Ring$
94	39	ad3antrrr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land z \in ℕ_{0}) \to {mulGrp}_{A} \in Mnd$
95		simpr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land z \in ℕ_{0}) \to z \in ℕ_{0}$
96	42	adantr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land z \in ℕ_{0}) \to M \in B$
97	36 16 94 95 96	mulgnn0cld	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land z \in ℕ_{0}) \to z \underset{˙}{\times} M \in B$
98	93 97	jca	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land z \in ℕ_{0}) \to (A \in Ring \land z \underset{˙}{\times} M \in B)$
99	98	adantr	$⊢ (((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land z \in ℕ_{0}) \land G (z) = 0_{Y}) \to (A \in Ring \land z \underset{˙}{\times} M \in B)$
100	2 55 24	ringrz	$⊢ (A \in Ring \land z \underset{˙}{\times} M \in B) \to (z \underset{˙}{\times} M) \cdot_{A} 0_{A} = 0_{A}$
101	99 100	syl	$⊢ (((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land z \in ℕ_{0}) \land G (z) = 0_{Y}) \to (z \underset{˙}{\times} M) \cdot_{A} 0_{A} = 0_{A}$
102	83 92 101	3eqtrd	$⊢ (((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land z \in ℕ_{0}) \land G (z) = 0_{Y}) \to ⦋ z / n ⦌ ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = 0_{A}$
103	102	ex	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land z \in ℕ_{0}) \to (G (z) = 0_{Y} \to ⦋ z / n ⦌ ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = 0_{A})$
104	103	adantlr	$⊢ (((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land w \in ℕ_{0}) \land z \in ℕ_{0}) \to (G (z) = 0_{Y} \to ⦋ z / n ⦌ ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = 0_{A})$
105	104	imim2d	$⊢ (((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land w \in ℕ_{0}) \land z \in ℕ_{0}) \to ((w < z \to G (z) = 0_{Y}) \to (w < z \to ⦋ z / n ⦌ ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = 0_{A}))$
106	105	ralimdva	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land w \in ℕ_{0}) \to (\forall z \in ℕ_{0} (w < z \to G (z) = 0_{Y}) \to \forall z \in ℕ_{0} (w < z \to ⦋ z / n ⦌ ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = 0_{A}))$
107	106	reximdva	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to (\exists w \in ℕ_{0} \forall z \in ℕ_{0} (w < z \to G (z) = 0_{Y}) \to \exists w \in ℕ_{0} \forall z \in ℕ_{0} (w < z \to ⦋ z / n ⦌ ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = 0_{A}))$
108	70 107	syld	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to ({finSupp}_{0_{Y}} (G) \to \exists w \in ℕ_{0} \forall z \in ℕ_{0} (w < z \to ⦋ z / n ⦌ ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = 0_{A}))$
109	62 108	mpd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to \exists w \in ℕ_{0} \forall z \in ℕ_{0} (w < z \to ⦋ z / n ⦌ ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = 0_{A})$
110	59 60 109	mptnn0fsupp	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to {finSupp}_{0_{A}} ((n \in ℕ_{0} ⟼ (n \underset{˙}{\times} M) \cdot_{A} U (G (n))))$
111	2 24 30 32 58 110	gsumcl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) \in B$
112	15 1 2 8	m2cpminvid	$⊢ (N \in Fin \land R \in Ring \land \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) \in B) \to U (T (\underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))))) = \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \cdot_{A} U (G (n)))$
113	20 23 111 112	syl3anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to U (T (\underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))))) = \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \cdot_{A} U (G (n)))$
114	3 4	pmatring	$⊢ (N \in Fin \land R \in Ring) \to Y \in Ring$
115	19 22 114	syl2anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Ring$
116		ringmnd	$⊢ Y \in Ring \to Y \in Mnd$
117	115 116	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Mnd$
118	117	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 Mnd$
119	8 1 2 3 4 12	mat2pmatghm	$⊢ (N \in Fin \land R \in Ring) \to T \in (A GrpHom Y)$
120	20 23 119	syl2anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to T \in (A GrpHom Y)$
121		ghmmhm	$⊢ T \in (A GrpHom Y) \to T \in (A MndHom Y)$
122	120 121	syl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to T \in (A MndHom Y)$
123	37	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}) \to A \in Ring$
124	21 46	sylan2	$⊢ (N \in Fin \land R \in CRing) \to U : N ConstPolyMat R ⟶ B$
125	124	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to U : N ConstPolyMat R ⟶ B$
126	125	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}) \to U : N ConstPolyMat R ⟶ B$
127	126 53	ffvelcdmd	$⊢ ((((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}) \to U (G (n)) \in B$
128	123 44 127 56	syl3anc	$⊢ ((((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}) \to (n \underset{˙}{\times} M) \cdot_{A} U (G (n)) \in B$
129	2 24 30 118 32 122 128 110	gsummptmhm	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to \underset{n \in ℕ_{0}}{\sum_{Y}} T ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = T (\underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))))$
130	8 1 2 3 4 12	mat2pmatrhm	$⊢ (N \in Fin \land R \in CRing) \to T \in (A RingHom Y)$
131	130	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T \in (A RingHom Y)$
132	131	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}) \to T \in (A RingHom Y)$
133	2 55 5	rhmmul	$⊢ (T \in (A RingHom Y) \land n \underset{˙}{\times} M \in B \land U (G (n)) \in B) \to T ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = T (n \underset{˙}{\times} M) \underset{˙}{\times} T (U (G (n)))$
134	132 44 127 133	syl3anc	$⊢ ((((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}) \to T ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = T (n \underset{˙}{\times} M) \underset{˙}{\times} T (U (G (n)))$
135	8 1 2 3 4 12	mat2pmatmhm	$⊢ (N \in Fin \land R \in CRing) \to T \in ({mulGrp}_{A} MndHom {mulGrp}_{Y})$
136	135	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T \in ({mulGrp}_{A} MndHom {mulGrp}_{Y})$
137	136	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}) \to T \in ({mulGrp}_{A} MndHom {mulGrp}_{Y})$
138	36 16 17	mhmmulg	$⊢ (T \in ({mulGrp}_{A} MndHom {mulGrp}_{Y}) \land n \in ℕ_{0} \land M \in B) \to T (n \underset{˙}{\times} M) = n E T (M)$
139	137 41 43 138	syl3anc	$⊢ ((((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}) \to T (n \underset{˙}{\times} M) = n E T (M)$
140	19	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}) \to N \in Fin$
141	22	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}) \to R \in Ring$
142	45 15 8	m2cpminvid2	$⊢ (N \in Fin \land R \in Ring \land G (n) \in (N ConstPolyMat R)) \to T (U (G (n))) = G (n)$
143	140 141 53 142	syl3anc	$⊢ ((((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}) \to T (U (G (n))) = G (n)$
144	139 143	oveq12d	$⊢ ((((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}) \to T (n \underset{˙}{\times} M) \underset{˙}{\times} T (U (G (n))) = (n E T (M)) \underset{˙}{\times} G (n)$
145	134 144	eqtrd	$⊢ ((((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}) \to T ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = (n E T (M)) \underset{˙}{\times} G (n)$
146	145	mpteq2dva	$⊢ (((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} ⟼ T ((n \underset{˙}{\times} M) \cdot_{A} U (G (n)))) = (n \in ℕ_{0} ⟼ (n E T (M)) \underset{˙}{\times} G (n))$
147	146	oveq2d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to \underset{n \in ℕ_{0}}{\sum_{Y}} T ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = \underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n))$
148	129 147	eqtr3d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to T (\underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \cdot_{A} U (G (n)))) = \underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n))$
149	148	fveq2d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to U (T (\underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))))) = U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n)))$
150	113 149	eqtr3d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \cdot_{A} U (G (n))) = U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n)))$
151	18 150	sylan9eqr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \cdot_{A} U (G (n)))) \to \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n)))$
152	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 55	cayhamlem3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (K) (n) \underset{˙}{*} (n \underset{˙}{\times} M)) = \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \cdot_{A} U (G (n)))$
153	151 152	reximddv2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (K) (n) \underset{˙}{*} (n \underset{˙}{\times} M)) = U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n)))$

Metamath Proof Explorer

Theorem cayhamlem4

Proof