chcoeffeqlem

Description: Lemma for chcoeffeq . (Contributed by AV, 21-Nov-2019) (Proof shortened by AV, 7-Dec-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$
Assertion	chcoeffeqlem	$⊢ ((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_{{Poly}_{1} (A)}} (U (G (n)) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))) = \underset{n \in ℕ_{0}}{\sum_{{Poly}_{1} (A)}} (({coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1}) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))) \to \forall n \in ℕ_{0} U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1})$

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		eqid	$⊢ {Poly}_{1} (A) = {Poly}_{1} (A)$
17		eqid	$⊢ {var}_{1} (A) = {var}_{1} (A)$
18		eqid	$⊢ \cdot_{{mulGrp}_{{Poly}_{1} (A)}} = \cdot_{{mulGrp}_{{Poly}_{1} (A)}}$
19		crngring	$⊢ R \in CRing \to R \in Ring$
20	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
21	19 20	sylan2	$⊢ (N \in Fin \land R \in CRing) \to A \in Ring$
22	21	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to A \in Ring$
23	22	adantr	$⊢ ((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$
24		eqid	$⊢ \cdot_{{Poly}_{1} (A)} = \cdot_{{Poly}_{1} (A)}$
25		eqid	$⊢ 0_{A} = 0_{A}$
26		eqid	$⊢ N ConstPolyMat R = N ConstPolyMat R$
27		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
28		eqid	$⊢ 1_{Y} = 1_{Y}$
29		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
30		eqid	$⊢ ({var}_{1} (R) \cdot_{Y} 1_{Y}) \underset{˙}{-} T (M) = ({var}_{1} (R) \cdot_{Y} 1_{Y}) \underset{˙}{-} T (M)$
31		eqid	$⊢ N maAdju P = N maAdju P$
32	1 2 3 4 8 5 6 7 11 26 27 28 29 30 31 12 16 17 24 18 15	cpmadumatpolylem1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to U \circ G \in (B^{ℕ_{0}})$
33	32	anasss	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to U \circ G \in (B^{ℕ_{0}})$
34	1 2 3 4 5 6 7 8 11 26	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$
35	19 34	syl3anl2	$⊢ ((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$
36	35	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land U \circ G \in (B^{ℕ_{0}})) \to G : ℕ_{0} ⟶ N ConstPolyMat R$
37		fvco3	$⊢ (G : ℕ_{0} ⟶ N ConstPolyMat R \land l \in ℕ_{0}) \to (U \circ G) (l) = U (G (l))$
38	37	eqcomd	$⊢ (G : ℕ_{0} ⟶ N ConstPolyMat R \land l \in ℕ_{0}) \to U (G (l)) = (U \circ G) (l)$
39	36 38	sylan	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land U \circ G \in (B^{ℕ_{0}})) \land l \in ℕ_{0}) \to U (G (l)) = (U \circ G) (l)$
40		elmapi	$⊢ U \circ G \in (B^{ℕ_{0}}) \to (U \circ G) : ℕ_{0} ⟶ B$
41	40	adantl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land U \circ G \in (B^{ℕ_{0}})) \to (U \circ G) : ℕ_{0} ⟶ B$
42	41	ffvelrnda	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land U \circ G \in (B^{ℕ_{0}})) \land l \in ℕ_{0}) \to (U \circ G) (l) \in B$
43	39 42	eqeltrd	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land U \circ G \in (B^{ℕ_{0}})) \land l \in ℕ_{0}) \to U (G (l)) \in B$
44	43	ralrimiva	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land U \circ G \in (B^{ℕ_{0}})) \to \forall l \in ℕ_{0} U (G (l)) \in B$
45	33 44	mpdan	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \forall l \in ℕ_{0} U (G (l)) \in B$
46	19	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
47	46	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in Ring)$
48	47	adantr	$⊢ ((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)$
49	1 2 26 15	cpm2mf	$⊢ (N \in Fin \land R \in Ring) \to U : N ConstPolyMat R ⟶ B$
50	48 49	syl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to U : N ConstPolyMat R ⟶ B$
51		fcompt	$⊢ (U : N ConstPolyMat R ⟶ B \land G : ℕ_{0} ⟶ N ConstPolyMat R) \to U \circ G = (l \in ℕ_{0} ⟼ U (G (l)))$
52	50 35 51	syl2anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to U \circ G = (l \in ℕ_{0} ⟼ U (G (l)))$
53	1 2 3 4 8 5 6 7 11 26 27 28 29 30 31 12 16 17 24 18 15	cpmadumatpolylem2	$⊢ (((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}} ((U \circ G))$
54	53	anasss	$⊢ ((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}} ((U \circ G))$
55	52 54	eqbrtrrd	$⊢ ((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}} ((l \in ℕ_{0} ⟼ U (G (l))))$
56		simpll1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land l \in ℕ_{0}) \to N \in Fin$
57	19	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
58	57	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land l \in ℕ_{0}) \to R \in Ring$
59		eqid	$⊢ {Base}_{P} = {Base}_{P}$
60	9 1 2 3 59	chpmatply1	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) \in {Base}_{P}$
61	10 60	eqeltrid	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to K \in {Base}_{P}$
62		eqid	$⊢ {coe}_{1} (K) = {coe}_{1} (K)$
63		eqid	$⊢ {Base}_{R} = {Base}_{R}$
64	62 59 3 63	coe1fvalcl	$⊢ (K \in {Base}_{P} \land l \in ℕ_{0}) \to {coe}_{1} (K) (l) \in {Base}_{R}$
65	61 64	sylan	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land l \in ℕ_{0}) \to {coe}_{1} (K) (l) \in {Base}_{R}$
66	65	adantlr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land l \in ℕ_{0}) \to {coe}_{1} (K) (l) \in {Base}_{R}$
67	2 13	ringidcl	$⊢ A \in Ring \to \underset{˙}{1} \in B$
68	22 67	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \underset{˙}{1} \in B$
69	68	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land l \in ℕ_{0}) \to \underset{˙}{1} \in B$
70	63 1 2 14	matvscl	$⊢ ((N \in Fin \land R \in Ring) \land ({coe}_{1} (K) (l) \in {Base}_{R} \land \underset{˙}{1} \in B)) \to {coe}_{1} (K) (l) \underset{˙}{*} \underset{˙}{1} \in B$
71	56 58 66 69 70	syl22anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land l \in ℕ_{0}) \to {coe}_{1} (K) (l) \underset{˙}{*} \underset{˙}{1} \in B$
72	71	ralrimiva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \forall l \in ℕ_{0} {coe}_{1} (K) (l) \underset{˙}{*} \underset{˙}{1} \in B$
73		nn0ex	$⊢ ℕ_{0} \in V$
74	73	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$
75	1	matlmod	$⊢ (N \in Fin \land R \in Ring) \to A \in LMod$
76	19 75	sylan2	$⊢ (N \in Fin \land R \in CRing) \to A \in LMod$
77	76	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to A \in LMod$
78	77	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to A \in LMod$
79		eqidd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to Scalar (A) = Scalar (A)$
80		fvexd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land l \in ℕ_{0}) \to {coe}_{1} (K) (l) \in V$
81		eqid	$⊢ 0_{Scalar (A)} = 0_{Scalar (A)}$
82	1	matsca2	$⊢ (N \in Fin \land R \in CRing) \to R = Scalar (A)$
83	82	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R = Scalar (A)$
84	83 57	eqeltrrd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Scalar (A) \in Ring$
85	83	eqcomd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Scalar (A) = R$
86	85	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Poly}_{1} (Scalar (A)) = {Poly}_{1} (R)$
87	86 3	eqtr4di	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Poly}_{1} (Scalar (A)) = P$
88	87	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Base}_{{Poly}_{1} (Scalar (A))} = {Base}_{P}$
89	61 88	eleqtrrd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to K \in {Base}_{{Poly}_{1} (Scalar (A))}$
90		eqid	$⊢ {Poly}_{1} (Scalar (A)) = {Poly}_{1} (Scalar (A))$
91		eqid	$⊢ {Base}_{{Poly}_{1} (Scalar (A))} = {Base}_{{Poly}_{1} (Scalar (A))}$
92	90 91 81	mptcoe1fsupp	$⊢ (Scalar (A) \in Ring \land K \in {Base}_{{Poly}_{1} (Scalar (A))}) \to {finSupp}_{0_{Scalar (A)}} ((l \in ℕ_{0} ⟼ {coe}_{1} (K) (l)))$
93	84 89 92	syl2anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {finSupp}_{0_{Scalar (A)}} ((l \in ℕ_{0} ⟼ {coe}_{1} (K) (l)))$
94	93	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to {finSupp}_{0_{Scalar (A)}} ((l \in ℕ_{0} ⟼ {coe}_{1} (K) (l)))$
95	74 78 79 2 80 69 25 81 14 94	mptscmfsupp0	$⊢ ((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}} ((l \in ℕ_{0} ⟼ {coe}_{1} (K) (l) \underset{˙}{*} \underset{˙}{1}))$
96		2fveq3	$⊢ n = l \to U (G (n)) = U (G (l))$
97		oveq1	$⊢ n = l \to n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A) = l \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A)$
98	96 97	oveq12d	$⊢ n = l \to U (G (n)) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A)) = U (G (l)) \cdot_{{Poly}_{1} (A)} (l \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))$
99	98	cbvmptv	$⊢ (n \in ℕ_{0} ⟼ U (G (n)) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))) = (l \in ℕ_{0} ⟼ U (G (l)) \cdot_{{Poly}_{1} (A)} (l \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A)))$
100	99	oveq2i	$⊢ \underset{n \in ℕ_{0}}{\sum_{{Poly}_{1} (A)}} (U (G (n)) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))) = \underset{l \in ℕ_{0}}{\sum_{{Poly}_{1} (A)}} (U (G (l)) \cdot_{{Poly}_{1} (A)} (l \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A)))$
101	100	a1i	$⊢ ((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_{{Poly}_{1} (A)}} (U (G (n)) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))) = \underset{l \in ℕ_{0}}{\sum_{{Poly}_{1} (A)}} (U (G (l)) \cdot_{{Poly}_{1} (A)} (l \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A)))$
102		fveq2	$⊢ n = l \to {coe}_{1} (K) (n) = {coe}_{1} (K) (l)$
103	102	oveq1d	$⊢ n = l \to {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1}$
104	103 97	oveq12d	$⊢ n = l \to ({coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1}) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A)) = ({coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1}) \cdot_{{Poly}_{1} (A)} (l \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))$
105	104	cbvmptv	$⊢ (n \in ℕ_{0} ⟼ ({coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1}) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))) = (l \in ℕ_{0} ⟼ ({coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1}) \cdot_{{Poly}_{1} (A)} (l \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A)))$
106	105	oveq2i	$⊢ \underset{n \in ℕ_{0}}{\sum_{{Poly}_{1} (A)}} (({coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1}) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))) = \underset{l \in ℕ_{0}}{\sum_{{Poly}_{1} (A)}} (({coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1}) \cdot_{{Poly}_{1} (A)} (l \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A)))$
107	106	a1i	$⊢ ((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_{{Poly}_{1} (A)}} (({coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1}) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))) = \underset{l \in ℕ_{0}}{\sum_{{Poly}_{1} (A)}} (({coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1}) \cdot_{{Poly}_{1} (A)} (l \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A)))$
108	16 17 18 23 2 24 25 45 55 72 95 101 107	gsumply1eq	$⊢ ((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_{{Poly}_{1} (A)}} (U (G (n)) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))) = \underset{n \in ℕ_{0}}{\sum_{{Poly}_{1} (A)}} (({coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1}) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))) \leftrightarrow \forall l \in ℕ_{0} U (G (l)) = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1})$
109	108	biimpa	$⊢ (((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_{{Poly}_{1} (A)}} (U (G (n)) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))) = \underset{n \in ℕ_{0}}{\sum_{{Poly}_{1} (A)}} (({coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1}) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A)))) \to \forall l \in ℕ_{0} U (G (l)) = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1}$
110	96 103	eqeq12d	$⊢ n = l \to (U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} \leftrightarrow U (G (l)) = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1})$
111	110	cbvralvw	$⊢ \forall n \in ℕ_{0} U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} \leftrightarrow \forall l \in ℕ_{0} U (G (l)) = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1}$
112	109 111	sylibr	$⊢ (((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_{{Poly}_{1} (A)}} (U (G (n)) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))) = \underset{n \in ℕ_{0}}{\sum_{{Poly}_{1} (A)}} (({coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1}) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A)))) \to \forall n \in ℕ_{0} U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1}$
113	112	ex	$⊢ ((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_{{Poly}_{1} (A)}} (U (G (n)) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))) = \underset{n \in ℕ_{0}}{\sum_{{Poly}_{1} (A)}} (({coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1}) \cdot_{{Poly}_{1} (A)} (n \cdot_{{mulGrp}_{{Poly}_{1} (A)}} {var}_{1} (A))) \to \forall n \in ℕ_{0} U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1})$

Metamath Proof Explorer

Theorem chcoeffeqlem

Proof