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