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	19 22 25	syl2anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to A \in Ring$
36		eqid	$⊢ {mulGrp}_{A} = {mulGrp}_{A}$
37	36	ringmgp	$⊢ A \in Ring \to {mulGrp}_{A} \in Mnd$
38	35 37	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{A} \in Mnd$
39	38	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$
40		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}$
41		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$
42	41	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$
43	36 2	mgpbas	$⊢ B = {Base}_{{mulGrp}_{A}}$
44	43 16	mulgnn0cl	$⊢ ({mulGrp}_{A} \in Mnd \land n \in ℕ_{0} \land M \in B) \to n \underset{˙}{\times} M \in B$
45	39 40 42 44	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 \in B$
46		eqid	$⊢ N ConstPolyMat R = N ConstPolyMat R$
47	1 2 46 15	cpm2mf	$⊢ (N \in Fin \land R \in Ring) \to U : N ConstPolyMat R ⟶ B$
48	19 22 47	syl2anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to U : N ConstPolyMat R ⟶ B$
49	48	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$
50		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 ℕ$
51		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)})$
52	1 2 3 4 5 6 7 8 11 46	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$
53	20 23 41 50 51 52	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$
54	53	ffvelrnda	$⊢ ((((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)$
55	49 54	ffvelrnd	$⊢ ((((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$
56		eqid	$⊢ \cdot_{A} = \cdot_{A}$
57	2 56	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$
58	34 45 55 57	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$
59	58	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$
60		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$
61		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$
62	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)$
63	62	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)$
64		ovex	$⊢ N ConstPolyMat R \in V$
65	64 31	pm3.2i	$⊢ (N ConstPolyMat R \in V \land ℕ_{0} \in V)$
66		elmapg	$⊢ (N ConstPolyMat R \in V \land ℕ_{0} \in V) \to (G \in ({(N ConstPolyMat R)}^{ℕ_{0}}) \leftrightarrow G : ℕ_{0} ⟶ N ConstPolyMat R)$
67	65 66	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)$
68	53 67	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}})$
69		fvex	$⊢ 0_{Y} \in V$
70		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}))$
71	68 69 70	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}))$
72		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))$
73		csbov1g	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ (n \underset{˙}{\times} M) = ⦋ z / n ⦌ n \underset{˙}{\times} M$
74		csbvarg	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ n = z$
75	74	oveq1d	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ n \underset{˙}{\times} M = z \underset{˙}{\times} M$
76	73 75	eqtrd	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ (n \underset{˙}{\times} M) = z \underset{˙}{\times} M$
77		csbfv2g	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ U (G (n)) = U (⦋ z / n ⦌ G (n))$
78		csbfv	$⊢ ⦋ z / n ⦌ G (n) = G (z)$
79	78	a1i	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ G (n) = G (z)$
80	79	fveq2d	$⊢ z \in ℕ_{0} \to U (⦋ z / n ⦌ G (n)) = U (G (z))$
81	77 80	eqtrd	$⊢ z \in ℕ_{0} \to ⦋ z / n ⦌ U (G (n)) = U (G (z))$
82	76 81	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))$
83	72 82	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))$
84	83	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))$
85		fveq2	$⊢ G (z) = 0_{Y} \to U (G (z)) = U (0_{Y})$
86	19 22	jca	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in Ring)$
87	86	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \to (N \in Fin \land R \in Ring)$
88		eqid	$⊢ 0_{Y} = 0_{Y}$
89	1 15 3 4 24 88	m2cpminv0	$⊢ (N \in Fin \land R \in Ring) \to U (0_{Y}) = 0_{A}$
90	87 89	syl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \to U (0_{Y}) = 0_{A}$
91	90	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}$
92	85 91	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}$
93	92	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}$
94	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$
95	38	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$
96		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}$
97	41	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$
98	43 16	mulgnn0cl	$⊢ ({mulGrp}_{A} \in Mnd \land z \in ℕ_{0} \land M \in B) \to z \underset{˙}{\times} M \in B$
99	95 96 97 98	syl3anc	$⊢ ((((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$
100	94 99	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)$
101	100	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)$
102	2 56 24	ringrz	$⊢ (A \in Ring \land z \underset{˙}{\times} M \in B) \to (z \underset{˙}{\times} M) \cdot_{A} 0_{A} = 0_{A}$
103	101 102	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}$
104	84 93 103	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}$
105	104	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})$
106	105	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})$
107	106	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}))$
108	107	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}))$
109	108	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}))$
110	71 109	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}))$
111	63 110	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})$
112	60 61 111	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))))$
113	2 24 30 32 59 112	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$
114	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)))$
115	20 23 113 114	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)))$
116	3 4	pmatring	$⊢ (N \in Fin \land R \in Ring) \to Y \in Ring$
117	19 22 116	syl2anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Ring$
118		ringmnd	$⊢ Y \in Ring \to Y \in Mnd$
119	117 118	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Mnd$
120	119	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$
121	8 1 2 3 4 12	mat2pmatghm	$⊢ (N \in Fin \land R \in Ring) \to T \in (A GrpHom Y)$
122	20 23 121	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)$
123		ghmmhm	$⊢ T \in (A GrpHom Y) \to T \in (A MndHom Y)$
124	122 123	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)$
125	35	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$
126	21 47	sylan2	$⊢ (N \in Fin \land R \in CRing) \to U : N ConstPolyMat R ⟶ B$
127	126	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to U : N ConstPolyMat R ⟶ B$
128	127	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$
129	128 54	ffvelrnd	$⊢ ((((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$
130	125 45 129 57	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$
131	2 24 30 120 32 124 130 112	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))))$
132	8 1 2 3 4 12	mat2pmatrhm	$⊢ (N \in Fin \land R \in CRing) \to T \in (A RingHom Y)$
133	132	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T \in (A RingHom Y)$
134	133	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)$
135	2 56 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)))$
136	134 45 129 135	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)))$
137	8 1 2 3 4 12	mat2pmatmhm	$⊢ (N \in Fin \land R \in CRing) \to T \in ({mulGrp}_{A} MndHom {mulGrp}_{Y})$
138	137	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T \in ({mulGrp}_{A} MndHom {mulGrp}_{Y})$
139	138	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})$
140	43 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)$
141	139 40 42 140	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)$
142	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$
143	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$
144	46 15 8	m2cpminvid2	$⊢ (N \in Fin \land R \in Ring \land G (n) \in (N ConstPolyMat R)) \to T (U (G (n))) = G (n)$
145	142 143 54 144	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)$
146	141 145	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)$
147	136 146	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)$
148	147	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))$
149	148	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))$
150	131 149	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))$
151	150	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)))$
152	115 151	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)))$
153	18 152	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)))$
154	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 56	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)))$
155	153 154	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