Metamath Proof Explorer

Theorem cpmadumatpoly

Description: The product of the characteristic matrix of a given matrix and its adjunct represented as a polynomial over matrices. (Contributed by AV, 20-Nov-2019) (Revised by AV, 7-Dec-2019)

Ref Expression
Hypotheses cpmadumatpoly.a 
|- A = ( N Mat R )
cpmadumatpoly.b 
|- B = ( Base ` A )
cpmadumatpoly.p 
|- P = ( Poly1 ` R )
cpmadumatpoly.y 
|- Y = ( N Mat P )
cpmadumatpoly.t 
|- T = ( N matToPolyMat R )
cpmadumatpoly.r 
|- .X. = ( .r ` Y )
cpmadumatpoly.m0 
|- .- = ( -g ` Y )
cpmadumatpoly.0 
|- .0. = ( 0g ` Y )
cpmadumatpoly.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 ) ) ) ) ) ) ) )
cpmadumatpoly.s 
|- S = ( N ConstPolyMat R )
cpmadumatpoly.m1 
|- .x. = ( .s ` Y )
cpmadumatpoly.1 
|- .1. = ( 1r ` Y )
cpmadumatpoly.z 
|- Z = ( var1 ` R )
cpmadumatpoly.d 
|- D = ( ( Z .x. .1. ) .- ( T ` M ) )
cpmadumatpoly.j 
|- J = ( N maAdju P )
cpmadumatpoly.w 
|- W = ( Base ` Y )
cpmadumatpoly.q 
|- Q = ( Poly1 ` A )
cpmadumatpoly.x 
|- X = ( var1 ` A )
cpmadumatpoly.m2 
|- .* = ( .s ` Q )
cpmadumatpoly.e 
|- .^ = ( .g ` ( mulGrp ` Q ) )
cpmadumatpoly.u 
|- U = ( N cPolyMatToMat R )
cpmadumatpoly.i 
|- I = ( N pMatToMatPoly R )
Assertion cpmadumatpoly 
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( I ` ( D .X. ( J ` D ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) .* ( n .^ X ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cpmadumatpoly.a 
 |-  A = ( N Mat R )
2 cpmadumatpoly.b 
 |-  B = ( Base ` A )
3 cpmadumatpoly.p 
 |-  P = ( Poly1 ` R )
4 cpmadumatpoly.y 
 |-  Y = ( N Mat P )
5 cpmadumatpoly.t 
 |-  T = ( N matToPolyMat R )
6 cpmadumatpoly.r 
 |-  .X. = ( .r ` Y )
7 cpmadumatpoly.m0 
 |-  .- = ( -g ` Y )
8 cpmadumatpoly.0 
 |-  .0. = ( 0g ` Y )
9 cpmadumatpoly.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 ) ) ) ) ) ) ) )
10 cpmadumatpoly.s 
 |-  S = ( N ConstPolyMat R )
11 cpmadumatpoly.m1 
 |-  .x. = ( .s ` Y )
12 cpmadumatpoly.1 
 |-  .1. = ( 1r ` Y )
13 cpmadumatpoly.z 
 |-  Z = ( var1 ` R )
14 cpmadumatpoly.d 
 |-  D = ( ( Z .x. .1. ) .- ( T ` M ) )
15 cpmadumatpoly.j 
 |-  J = ( N maAdju P )
16 cpmadumatpoly.w 
 |-  W = ( Base ` Y )
17 cpmadumatpoly.q 
 |-  Q = ( Poly1 ` A )
18 cpmadumatpoly.x 
 |-  X = ( var1 ` A )
19 cpmadumatpoly.m2 
 |-  .* = ( .s ` Q )
20 cpmadumatpoly.e 
 |-  .^ = ( .g ` ( mulGrp ` Q ) )
21 cpmadumatpoly.u 
 |-  U = ( N cPolyMatToMat R )
22 cpmadumatpoly.i 
 |-  I = ( N pMatToMatPoly R )
23 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
24 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
25 eqeq1 
 |-  ( n = z -> ( n = 0 <-> z = 0 ) )
26 eqeq1 
 |-  ( n = z -> ( n = ( s + 1 ) <-> z = ( s + 1 ) ) )
27 breq2 
 |-  ( n = z -> ( ( s + 1 ) < n <-> ( s + 1 ) < z ) )
28 fvoveq1 
 |-  ( n = z -> ( b ` ( n - 1 ) ) = ( b ` ( z - 1 ) ) )
29 28 fveq2d 
 |-  ( n = z -> ( T ` ( b ` ( n - 1 ) ) ) = ( T ` ( b ` ( z - 1 ) ) ) )
30 2fveq3 
 |-  ( n = z -> ( T ` ( b ` n ) ) = ( T ` ( b ` z ) ) )
31 30 oveq2d 
 |-  ( n = z -> ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` z ) ) ) )
32 29 31 oveq12d 
 |-  ( n = z -> ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) = ( ( T ` ( b ` ( z - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` z ) ) ) ) )
33 27 32 ifbieq2d 
 |-  ( n = z -> if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) = if ( ( s + 1 ) < z , .0. , ( ( T ` ( b ` ( z - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` z ) ) ) ) ) )
34 26 33 ifbieq2d 
 |-  ( n = z -> if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) = if ( z = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < z , .0. , ( ( T ` ( b ` ( z - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` z ) ) ) ) ) ) )
35 25 34 ifbieq2d 
 |-  ( n = z -> 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 ) ) ) ) ) ) ) = if ( z = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( z = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < z , .0. , ( ( T ` ( b ` ( z - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` z ) ) ) ) ) ) ) )
36 35 cbvmptv 
 |-  ( 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 ) ) ) ) ) ) ) ) = ( z e. NN0 |-> if ( z = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( z = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < z , .0. , ( ( T ` ( b ` ( z - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` z ) ) ) ) ) ) ) )
37 9 36 eqtri 
 |-  G = ( z e. NN0 |-> if ( z = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( z = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < z , .0. , ( ( T ` ( b ` ( z - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` z ) ) ) ) ) ) ) )
38 1 2 3 4 5 13 23 11 6 12 24 7 14 15 8 37 cpmadugsum 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( D .X. ( J ` D ) ) = ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( G ` n ) ) ) ) )
39 simp1 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> N e. Fin )
40 39 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 )
41 crngring 
 |-  ( R e. CRing -> R e. Ring )
42 41 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
43 42 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 )
44 1 2 3 4 6 7 8 5 9 10 chfacfisfcpmat 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G : NN0 --> S )
45 41 44 syl3anl2 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G : NN0 --> S )
46 45 anassrs 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> G : NN0 --> S )
47 46 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. S )
48 10 21 5 m2cpminvid2 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( G ` n ) e. S ) -> ( T ` ( U ` ( G ` n ) ) ) = ( G ` n ) )
49 40 43 47 48 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 ) )
50 49 eqcomd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ n e. NN0 ) -> ( G ` n ) = ( T ` ( U ` ( G ` n ) ) ) )
51 50 oveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ n e. NN0 ) -> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( G ` n ) ) = ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( U ` ( G ` n ) ) ) ) )
52 51 mpteq2dva 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( G ` n ) ) ) = ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( U ` ( G ` n ) ) ) ) ) )
53 52 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( G ` n ) ) ) ) = ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( U ` ( G ` n ) ) ) ) ) ) )
54 53 eqeq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( D .X. ( J ` D ) ) = ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( G ` n ) ) ) ) <-> ( D .X. ( J ` D ) ) = ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( U ` ( G ` n ) ) ) ) ) ) ) )
55 fveq2 
 |-  ( ( D .X. ( J ` D ) ) = ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( U ` ( G ` n ) ) ) ) ) ) -> ( I ` ( D .X. ( J ` D ) ) ) = ( I ` ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( U ` ( G ` n ) ) ) ) ) ) ) )
56 3simpa 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. CRing ) )
57 56 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( N e. Fin /\ R e. CRing ) )
58 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 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 ) )
59 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 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 ) )
60 3 4 16 19 20 18 1 2 17 22 23 13 11 5 pm2mp 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( ( U o. G ) e. ( B ^m NN0 ) /\ ( U o. G ) finSupp ( 0g ` A ) ) ) -> ( I ` ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( ( U o. G ) ` n ) ) ) ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( ( U o. G ) ` n ) .* ( n .^ X ) ) ) ) )
61 57 58 59 60 syl12anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( I ` ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( ( U o. G ) ` n ) ) ) ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( ( U o. G ) ` n ) .* ( n .^ X ) ) ) ) )
62 fvco3 
 |-  ( ( G : NN0 --> S /\ n e. NN0 ) -> ( ( U o. G ) ` n ) = ( U ` ( G ` n ) ) )
63 62 eqcomd 
 |-  ( ( G : NN0 --> S /\ n e. NN0 ) -> ( U ` ( G ` n ) ) = ( ( U o. G ) ` n ) )
64 46 63 sylan 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ n e. NN0 ) -> ( U ` ( G ` n ) ) = ( ( U o. G ) ` n ) )
65 64 fveq2d 
 |-  ( ( ( ( ( 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 ) ) ) = ( T ` ( ( U o. G ) ` n ) ) )
66 65 oveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ n e. NN0 ) -> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( U ` ( G ` n ) ) ) ) = ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( ( U o. G ) ` n ) ) ) )
67 66 mpteq2dva 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( U ` ( G ` n ) ) ) ) ) = ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( ( U o. G ) ` n ) ) ) ) )
68 67 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( U ` ( G ` n ) ) ) ) ) ) = ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( ( U o. G ) ` n ) ) ) ) ) )
69 68 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( I ` ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( U ` ( G ` n ) ) ) ) ) ) ) = ( I ` ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( ( U o. G ) ` n ) ) ) ) ) ) )
70 64 oveq1d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ n e. NN0 ) -> ( ( U ` ( G ` n ) ) .* ( n .^ X ) ) = ( ( ( U o. G ) ` n ) .* ( n .^ X ) ) )
71 70 mpteq2dva 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( n e. NN0 |-> ( ( U ` ( G ` n ) ) .* ( n .^ X ) ) ) = ( n e. NN0 |-> ( ( ( U o. G ) ` n ) .* ( n .^ X ) ) ) )
72 71 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( Q gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) .* ( n .^ X ) ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( ( U o. G ) ` n ) .* ( n .^ X ) ) ) ) )
73 61 69 72 3eqtr4d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( I ` ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( U ` ( G ` n ) ) ) ) ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) .* ( n .^ X ) ) ) ) )
74 55 73 sylan9eqr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ ( D .X. ( J ` D ) ) = ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( U ` ( G ` n ) ) ) ) ) ) ) -> ( I ` ( D .X. ( J ` D ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) .* ( n .^ X ) ) ) ) )
75 74 ex 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( D .X. ( J ` D ) ) = ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( T ` ( U ` ( G ` n ) ) ) ) ) ) -> ( I ` ( D .X. ( J ` D ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) .* ( n .^ X ) ) ) ) ) )
76 54 75 sylbid 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( D .X. ( J ` D ) ) = ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( G ` n ) ) ) ) -> ( I ` ( D .X. ( J ` D ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) .* ( n .^ X ) ) ) ) ) )
77 76 reximdva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) -> ( E. b e. ( B ^m ( 0 ... s ) ) ( D .X. ( J ` D ) ) = ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( G ` n ) ) ) ) -> E. b e. ( B ^m ( 0 ... s ) ) ( I ` ( D .X. ( J ` D ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) .* ( n .^ X ) ) ) ) ) )
78 77 reximdva 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( D .X. ( J ` D ) ) = ( Y gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` P ) ) Z ) .x. ( G ` n ) ) ) ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( I ` ( D .X. ( J ` D ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) .* ( n .^ X ) ) ) ) ) )
79 38 78 mpd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( I ` ( D .X. ( J ` D ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( U ` ( G ` n ) ) .* ( n .^ X ) ) ) ) )