Metamath Proof Explorer

Theorem chcoeffeq

Description: The coefficients of the characteristic polynomial multiplied with the identity matrix represented by (transformed) ring elements obtained from the adjunct of the characteristic matrix. (Contributed by AV, 21-Nov-2019) (Proof shortened by AV, 8-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 chcoeffeq 
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) 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 
 |-  ( N ConstPolyMat R ) = ( N ConstPolyMat R )
17 eqid 
 |-  ( .s ` Y ) = ( .s ` Y )
18 eqid 
 |-  ( 1r ` Y ) = ( 1r ` Y )
19 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
20 eqid 
 |-  ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) = ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) )
21 eqid 
 |-  ( N maAdju P ) = ( N maAdju P )
22 eqid 
 |-  ( Poly1 ` A ) = ( Poly1 ` A )
23 eqid 
 |-  ( var1 ` A ) = ( var1 ` A )
24 eqid 
 |-  ( .s ` ( Poly1 ` A ) ) = ( .s ` ( Poly1 ` A ) )
25 eqid 
 |-  ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` A ) ) )
26 eqid 
 |-  ( N pMatToMatPoly R ) = ( N pMatToMatPoly R )
27 1 2 3 4 8 5 6 7 11 16 17 18 19 20 21 12 22 23 24 25 15 26 cpmadumatpoly 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) )
28 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
29 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
30 eqid 
 |-  ( K ( .s ` Y ) ( 1r ` Y ) ) = ( K ( .s ` Y ) ( 1r ` Y ) )
31 1 2 3 4 19 28 17 18 29 9 10 30 13 14 8 12 22 23 24 25 26 cpmidpmat 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* .1. ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) )
32 eqid 
 |-  ( N CharPlyMat R ) = ( N CharPlyMat R )
33 1 2 32 3 4 19 8 6 17 18 20 21 5 cpmadurid 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) = ( ( ( N CharPlyMat R ) ` M ) ( .s ` Y ) ( 1r ` Y ) ) )
34 9 fveq1i 
 |-  ( C ` M ) = ( ( N CharPlyMat R ) ` M )
35 10 34 eqtri 
 |-  K = ( ( N CharPlyMat R ) ` M )
36 35 a1i 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> K = ( ( N CharPlyMat R ) ` M ) )
37 36 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( N CharPlyMat R ) ` M ) = K )
38 37 oveq1d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( ( N CharPlyMat R ) ` M ) ( .s ` Y ) ( 1r ` Y ) ) = ( K ( .s ` Y ) ( 1r ` Y ) ) )
39 33 38 eqtrd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) = ( K ( .s ` Y ) ( 1r ` Y ) ) )
40 fveq2 
 |-  ( ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) = ( K ( .s ` Y ) ( 1r ` Y ) ) -> ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) )
41 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) ) -> ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) )
42 41 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) ) /\ ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* .1. ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) ) -> ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) )
43 simpr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) ) /\ ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* .1. ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) ) -> ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* .1. ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) )
44 42 43 eqeq12d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) ) /\ ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* .1. ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) ) -> ( ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) <-> ( ( 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 ) ) ) ) ) ) )
45 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 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. ) ) )
46 45 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( 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 |-> ( ( 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. ) ) )
47 46 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) ) /\ ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* .1. ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) ) -> ( ( ( 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. ) ) )
48 44 47 sylbid 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) ) /\ ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* .1. ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) ) -> ( ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) -> A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) ) )
49 48 exp31 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) -> ( ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* .1. ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) -> ( ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) -> A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) ) ) ) )
50 49 com24 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) -> ( ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* .1. ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) -> ( ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) -> A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) ) ) ) )
51 40 50 syl5 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) = ( K ( .s ` Y ) ( 1r ` Y ) ) -> ( ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* .1. ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) -> ( ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) -> A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) ) ) ) )
52 51 ex 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) = ( K ( .s ` Y ) ( 1r ` Y ) ) -> ( ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* .1. ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) -> ( ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) -> A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) ) ) ) ) )
53 52 com24 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( ( N pMatToMatPoly R ) ` ( K ( .s ` Y ) ( 1r ` Y ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* .1. ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) -> ( ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) = ( K ( .s ` Y ) ( 1r ` Y ) ) -> ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) -> A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) ) ) ) ) )
54 31 39 53 mp2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) -> A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) ) ) )
55 54 impl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) -> A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) ) )
56 55 reximdva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) -> ( E. b e. ( B ^m ( 0 ... s ) ) ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) -> E. b e. ( B ^m ( 0 ... s ) ) A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) ) )
57 56 reximdva 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( ( N pMatToMatPoly R ) ` ( ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) .X. ( ( N maAdju P ) ` ( ( ( var1 ` R ) ( .s ` Y ) ( 1r ` Y ) ) .- ( T ` M ) ) ) ) ) = ( ( Poly1 ` A ) gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) ( .s ` ( Poly1 ` A ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` A ) ) ) ( var1 ` A ) ) ) ) ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) ) )
58 27 57 mpd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) )