Metamath Proof Explorer


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