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