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 โŠข ๐ด = ( ๐‘ Mat ๐‘… )
chcoeffeq.b โŠข ๐ต = ( Base โ€˜ ๐ด )
chcoeffeq.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
chcoeffeq.y โŠข ๐‘Œ = ( ๐‘ Mat ๐‘ƒ )
chcoeffeq.r โŠข ร— = ( .r โ€˜ ๐‘Œ )
chcoeffeq.s โŠข โˆ’ = ( -g โ€˜ ๐‘Œ )
chcoeffeq.0 โŠข 0 = ( 0g โ€˜ ๐‘Œ )
chcoeffeq.t โŠข ๐‘‡ = ( ๐‘ matToPolyMat ๐‘… )
chcoeffeq.c โŠข ๐ถ = ( ๐‘ CharPlyMat ๐‘… )
chcoeffeq.k โŠข ๐พ = ( ๐ถ โ€˜ ๐‘€ )
chcoeffeq.g โŠข ๐บ = ( ๐‘› โˆˆ โ„•0 โ†ฆ if ( ๐‘› = 0 , ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) , if ( ๐‘› = ( ๐‘  + 1 ) , ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) , if ( ( ๐‘  + 1 ) < ๐‘› , 0 , ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) ) ) ) )
chcoeffeq.w โŠข ๐‘Š = ( Base โ€˜ ๐‘Œ )
chcoeffeq.1 โŠข 1 = ( 1r โ€˜ ๐ด )
chcoeffeq.m โŠข โˆ— = ( ยท๐‘  โ€˜ ๐ด )
chcoeffeq.u โŠข ๐‘ˆ = ( ๐‘ cPolyMatToMat ๐‘… )
Assertion chcoeffeq ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ โˆƒ ๐‘  โˆˆ โ„• โˆƒ ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) = ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) )

Proof

Step Hyp Ref Expression
1 chcoeffeq.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
2 chcoeffeq.b โŠข ๐ต = ( Base โ€˜ ๐ด )
3 chcoeffeq.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
4 chcoeffeq.y โŠข ๐‘Œ = ( ๐‘ Mat ๐‘ƒ )
5 chcoeffeq.r โŠข ร— = ( .r โ€˜ ๐‘Œ )
6 chcoeffeq.s โŠข โˆ’ = ( -g โ€˜ ๐‘Œ )
7 chcoeffeq.0 โŠข 0 = ( 0g โ€˜ ๐‘Œ )
8 chcoeffeq.t โŠข ๐‘‡ = ( ๐‘ matToPolyMat ๐‘… )
9 chcoeffeq.c โŠข ๐ถ = ( ๐‘ CharPlyMat ๐‘… )
10 chcoeffeq.k โŠข ๐พ = ( ๐ถ โ€˜ ๐‘€ )
11 chcoeffeq.g โŠข ๐บ = ( ๐‘› โˆˆ โ„•0 โ†ฆ if ( ๐‘› = 0 , ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) , if ( ๐‘› = ( ๐‘  + 1 ) , ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) , if ( ( ๐‘  + 1 ) < ๐‘› , 0 , ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) ) ) ) )
12 chcoeffeq.w โŠข ๐‘Š = ( Base โ€˜ ๐‘Œ )
13 chcoeffeq.1 โŠข 1 = ( 1r โ€˜ ๐ด )
14 chcoeffeq.m โŠข โˆ— = ( ยท๐‘  โ€˜ ๐ด )
15 chcoeffeq.u โŠข ๐‘ˆ = ( ๐‘ cPolyMatToMat ๐‘… )
16 eqid โŠข ( ๐‘ ConstPolyMat ๐‘… ) = ( ๐‘ ConstPolyMat ๐‘… )
17 eqid โŠข ( ยท๐‘  โ€˜ ๐‘Œ ) = ( ยท๐‘  โ€˜ ๐‘Œ )
18 eqid โŠข ( 1r โ€˜ ๐‘Œ ) = ( 1r โ€˜ ๐‘Œ )
19 eqid โŠข ( var1 โ€˜ ๐‘… ) = ( var1 โ€˜ ๐‘… )
20 eqid โŠข ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) = ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) )
21 eqid โŠข ( ๐‘ maAdju ๐‘ƒ ) = ( ๐‘ maAdju ๐‘ƒ )
22 eqid โŠข ( Poly1 โ€˜ ๐ด ) = ( Poly1 โ€˜ ๐ด )
23 eqid โŠข ( var1 โ€˜ ๐ด ) = ( var1 โ€˜ ๐ด )
24 eqid โŠข ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) = ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) )
25 eqid โŠข ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) = ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) )
26 eqid โŠข ( ๐‘ pMatToMatPoly ๐‘… ) = ( ๐‘ pMatToMatPoly ๐‘… )
27 1 2 3 4 8 5 6 7 11 16 17 18 19 20 21 12 22 23 24 25 15 26 cpmadumatpoly โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ โˆƒ ๐‘  โˆˆ โ„• โˆƒ ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) )
28 eqid โŠข ( .g โ€˜ ( mulGrp โ€˜ ๐‘ƒ ) ) = ( .g โ€˜ ( mulGrp โ€˜ ๐‘ƒ ) )
29 eqid โŠข ( algSc โ€˜ ๐‘ƒ ) = ( algSc โ€˜ ๐‘ƒ )
30 eqid โŠข ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) = ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) )
31 1 2 3 4 19 28 17 18 29 9 10 30 13 14 8 12 22 23 24 25 26 cpmidpmat โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) )
32 eqid โŠข ( ๐‘ CharPlyMat ๐‘… ) = ( ๐‘ CharPlyMat ๐‘… )
33 1 2 32 3 4 19 8 6 17 18 20 21 5 cpmadurid โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) = ( ( ( ๐‘ CharPlyMat ๐‘… ) โ€˜ ๐‘€ ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) )
34 9 fveq1i โŠข ( ๐ถ โ€˜ ๐‘€ ) = ( ( ๐‘ CharPlyMat ๐‘… ) โ€˜ ๐‘€ )
35 10 34 eqtri โŠข ๐พ = ( ( ๐‘ CharPlyMat ๐‘… ) โ€˜ ๐‘€ )
36 35 a1i โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐พ = ( ( ๐‘ CharPlyMat ๐‘… ) โ€˜ ๐‘€ ) )
37 36 eqcomd โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ( ๐‘ CharPlyMat ๐‘… ) โ€˜ ๐‘€ ) = ๐พ )
38 37 oveq1d โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ( ( ๐‘ CharPlyMat ๐‘… ) โ€˜ ๐‘€ ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) = ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) )
39 33 38 eqtrd โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) = ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) )
40 fveq2 โŠข ( ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) = ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โ†’ ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) )
41 simpr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) ) โ†’ ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) )
42 41 adantr โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) ) โˆง ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) ) โ†’ ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) )
43 simpr โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) ) โˆง ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) ) โ†’ ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) )
44 42 43 eqeq12d โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) ) โˆง ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) โ†” ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) ) )
45 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 chcoeffeqlem โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) = ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ) )
46 45 adantr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) ) โ†’ ( ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) = ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ) )
47 46 adantr โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) ) โˆง ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) ) โ†’ ( ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) = ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ) )
48 44 47 sylbid โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) ) โˆง ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) โ†’ โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) = ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ) )
49 48 exp31 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) โ†’ โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) = ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ) ) ) )
50 49 com24 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) = ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ) ) ) )
51 40 50 syl5 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) = ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) = ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ) ) ) )
52 51 ex โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ( ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) = ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) = ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ) ) ) ) )
53 52 com24 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ ( ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) = ( ๐พ ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โ†’ ( ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) = ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ) ) ) ) )
54 31 39 53 mp2d โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) = ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ) ) )
55 54 impl โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ( ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) = ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ) )
56 55 reximdva โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โ†’ ( โˆƒ ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ โˆƒ ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) = ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ) )
57 56 reximdva โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( โˆƒ ๐‘  โˆˆ โ„• โˆƒ ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ( ( ๐‘ pMatToMatPoly ๐‘… ) โ€˜ ( ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ร— ( ( ๐‘ maAdju ๐‘ƒ ) โ€˜ ( ( ( var1 โ€˜ ๐‘… ) ( ยท๐‘  โ€˜ ๐‘Œ ) ( 1r โ€˜ ๐‘Œ ) ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) ) ) ) ) = ( ( Poly1 โ€˜ ๐ด ) ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) ( ยท๐‘  โ€˜ ( Poly1 โ€˜ ๐ด ) ) ( ๐‘› ( .g โ€˜ ( mulGrp โ€˜ ( Poly1 โ€˜ ๐ด ) ) ) ( var1 โ€˜ ๐ด ) ) ) ) ) โ†’ โˆƒ ๐‘  โˆˆ โ„• โˆƒ ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) = ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) ) )
58 27 57 mpd โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ โˆƒ ๐‘  โˆˆ โ„• โˆƒ ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘ˆ โ€˜ ( ๐บ โ€˜ ๐‘› ) ) = ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— 1 ) )