Metamath Proof Explorer

Theorem 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 = ( 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 )
cayhamlem.e1 
|- .^ = ( .g ` ( mulGrp ` A ) )
cayhamlem.e2 
|- E = ( .g ` ( mulGrp ` Y ) )
Assertion cayhamlem4 
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) ) ) = ( U ` ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) ) )

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